| Package | Description |
|---|---|
| org.sat4j |
Contains a command line launcher for the SAT solvers.
|
| org.sat4j.minisat.constraints |
Implementations of various constraints for MiniSAT.
|
| org.sat4j.minisat.constraints.card |
Implementations of cardinality constraints.
|
| org.sat4j.minisat.constraints.cnf |
Implementations of clausal constraints.
|
| org.sat4j.minisat.core |
Implementation of the MiniSAT solver skeleton.
|
| org.sat4j.opt |
Built-in optimization framework.
|
| org.sat4j.reader |
Some utility classes to read problems from plain text files.
|
| org.sat4j.specs |
Those classes are intended for users dealing with SAT solvers as black boxes.
|
| org.sat4j.tools |
Tools to be used on top of an
ISolver. |
| org.sat4j.tools.encoding |
Implementation of different encodings.
|
| org.sat4j.tools.xplain |
Implementation of an explanation engine in case of unsatisfiability.
|
| Modifier and Type | Method and Description |
|---|---|
protected IProblem |
AbstractLauncher.readProblem(String problemname)
Reads a problem file from the command line.
|
| Modifier and Type | Method and Description |
|---|---|
Constr |
AbstractDataStructureFactory.createCardinalityConstraint(IVecInt literals,
int degree) |
Constr |
MixedDataStructureSingleWL.createCardinalityConstraint(IVecInt literals,
int degree) |
Constr |
CardinalityDataStructure.createCardinalityConstraint(IVecInt literals,
int degree) |
Constr |
MixedDataStructureDanielHT.createCardinalityConstraint(IVecInt literals,
int degree) |
Constr |
MixedDataStructureDanielWL.createCardinalityConstraint(IVecInt literals,
int degree) |
Constr |
CardinalityDataStructureYanMin.createCardinalityConstraint(IVecInt literals,
int degree) |
Constr |
CardinalityDataStructureYanMax.createCardinalityConstraint(IVecInt literals,
int degree) |
Constr |
ClausalDataStructureWL.createClause(IVecInt literals) |
Constr |
MixedDataStructureSingleWL.createClause(IVecInt literals) |
Constr |
CardinalityDataStructure.createClause(IVecInt literals) |
Constr |
MixedDataStructureDanielHT.createClause(IVecInt literals) |
Constr |
MixedDataStructureDanielWL.createClause(IVecInt literals) |
Constr |
CardinalityDataStructureYanMin.createClause(IVecInt literals) |
Constr |
CardinalityDataStructureYanMax.createClause(IVecInt literals) |
| Modifier and Type | Method and Description |
|---|---|
static Constr |
AtLeast.atLeastNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
int n) |
protected MinWatchCard |
MinWatchCard.computePropagation(UnitPropagationListener s) |
static Constr |
MaxWatchCard.maxWatchCardNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
boolean moreThan,
int degree)
Permet la cr?
|
static Constr |
MinWatchCard.minWatchCardNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
boolean moreThan,
int degree)
Constructs a cardinality constraint with a minimal set of watched
literals Permet la cr?
|
protected static int |
AtLeast.niceParameters(UnitPropagationListener s,
ILits voc,
IVecInt ps,
int deg) |
| Modifier and Type | Method and Description |
|---|---|
static IVecInt |
Clauses.sanityCheck(IVecInt ps,
ILits voc,
UnitPropagationListener s)
Perform some sanity check before constructing a clause a) if a literal is
assigned true, return null (the clause is satisfied) b) if a literal is
assigned false, remove it c) if a clause contains a literal and its
opposite (tautology) return null d) remove duplicate literals e) if the
clause is empty, return null f) if the clause if unit, transmit it to the
object responsible for unit propagation
|
| Modifier and Type | Method and Description |
|---|---|
void |
Solver.addAllClauses(IVec<IVecInt> clauses) |
IConstr |
Solver.addAtLeast(IVecInt literals,
int degree) |
IConstr |
Solver.addAtMost(IVecInt literals,
int degree) |
IConstr |
Solver.addBlockingClause(IVecInt literals) |
IConstr |
Solver.addClause(IVecInt literals) |
IConstr |
Solver.addExactly(IVecInt literals,
int n) |
Constr |
DataStructureFactory.createCardinalityConstraint(IVecInt literals,
int degree)
Create a cardinality constraint of the form sum li >= degree.
|
Constr |
DataStructureFactory.createClause(IVecInt literals) |
| Modifier and Type | Method and Description |
|---|---|
IConstr |
MaxSatDecorator.addClause(IVecInt literals) |
void |
MaxSatDecorator.discard() |
void |
MinOneDecorator.discard() |
void |
MaxSatDecorator.discardCurrentSolution() |
void |
MinOneDecorator.discardCurrentSolution() |
void |
MaxSatDecorator.forceObjectiveValueTo(Number forcedValue) |
void |
MinOneDecorator.forceObjectiveValueTo(Number forcedValue) |
| Modifier and Type | Method and Description |
|---|---|
protected void |
DimacsReader.flushConstraint() |
protected void |
GroupedCNFReader.flushConstraint() |
protected void |
JSONReader.handleCard(String constraint) |
protected boolean |
DimacsReader.handleLine() |
protected boolean |
GroupedCNFReader.handleLine() |
protected void |
JSONReader.handleNotHandled(String constraint) |
IProblem |
InstanceReader.parseInstance(InputStream in) |
IProblem |
AAGReader.parseInstance(InputStream in) |
IProblem |
JSONReader.parseInstance(InputStream in) |
IProblem |
LecteurDimacs.parseInstance(InputStream input) |
abstract IProblem |
Reader.parseInstance(InputStream in)
Read a file from a stream.
|
IProblem |
AIGReader.parseInstance(InputStream in) |
IProblem |
DimacsReader.parseInstance(InputStream in) |
IProblem |
Reader.parseInstance(Reader in)
Deprecated.
|
IProblem |
InstanceReader.parseInstance(String filename) |
IProblem |
Reader.parseInstance(String filename)
This is the usual method to feed a solver with a benchmark.
|
ISolver |
JSONReader.parseString(String json) |
protected void |
DimacsReader.readConstrs() |
| Modifier and Type | Method and Description |
|---|---|
void |
ISolver.addAllClauses(IVec<IVecInt> clauses)
Create clauses from a set of set of literals.
|
IConstr |
ISolver.addAtLeast(IVecInt literals,
int degree)
Create a cardinality constraint of the type "at least n of those literals
must be satisfied"
|
IConstr |
ISolver.addAtMost(IVecInt literals,
int degree)
Create a cardinality constraint of the type "at most n of those literals
must be satisfied"
|
IConstr |
ISolver.addBlockingClause(IVecInt literals)
Add a clause in order to prevent an assignment to occur.
|
IConstr |
ISolver.addClause(IVecInt literals)
Create a clause from a set of literals The literals are represented by
non null integers such that opposite literals a represented by opposite
values.
|
IConstr |
IGroupSolver.addClause(IVecInt literals,
int desc) |
IConstr |
ISolver.addExactly(IVecInt literals,
int n)
Create a cardinality constraint of the type
"exactly n of those literals must be satisfied".
|
void |
IOptimizationProblem.discard()
Deprecated.
|
void |
IOptimizationProblem.discardCurrentSolution()
Discard the current solution in the optimization problem.
|
void |
IOptimizationProblem.forceObjectiveValueTo(Number forcedValue)
Force the value of the objective function.
|
| Modifier and Type | Method and Description |
|---|---|
void |
AbstractOutputSolver.addAllClauses(IVec<IVecInt> clauses) |
void |
ManyCore.addAllClauses(IVec<IVecInt> clauses) |
void |
StatisticsSolver.addAllClauses(IVec<IVecInt> clauses) |
void |
SolverDecorator.addAllClauses(IVec<IVecInt> clauses) |
IConstr |
NegationDecorator.addAtLeast(IVecInt literals,
int degree) |
IConstr |
ManyCore.addAtLeast(IVecInt literals,
int degree) |
IConstr |
ClausalCardinalitiesDecorator.addAtLeast(IVecInt literals,
int k) |
IConstr |
DimacsOutputSolver.addAtLeast(IVecInt literals,
int degree) |
IConstr |
StatisticsSolver.addAtLeast(IVecInt literals,
int degree) |
IConstr |
DimacsStringSolver.addAtLeast(IVecInt literals,
int degree) |
IConstr |
SolverDecorator.addAtLeast(IVecInt literals,
int degree) |
IConstr |
NegationDecorator.addAtMost(IVecInt literals,
int degree) |
IConstr |
ManyCore.addAtMost(IVecInt literals,
int degree) |
IConstr |
ClausalCardinalitiesDecorator.addAtMost(IVecInt literals,
int k) |
IConstr |
DimacsOutputSolver.addAtMost(IVecInt literals,
int degree) |
IConstr |
StatisticsSolver.addAtMost(IVecInt literals,
int degree) |
IConstr |
DimacsStringSolver.addAtMost(IVecInt literals,
int degree) |
IConstr |
SolverDecorator.addAtMost(IVecInt literals,
int degree) |
IConstr |
AbstractOutputSolver.addBlockingClause(IVecInt literals) |
IConstr |
ManyCore.addBlockingClause(IVecInt literals) |
IConstr |
StatisticsSolver.addBlockingClause(IVecInt literals) |
IConstr |
SolverDecorator.addBlockingClause(IVecInt literals) |
IConstr |
NegationDecorator.addClause(IVecInt literals) |
IConstr |
ManyCore.addClause(IVecInt literals) |
IConstr |
FullClauseSelectorSolver.addClause(IVecInt literals) |
IConstr |
DimacsOutputSolver.addClause(IVecInt literals) |
IConstr |
StatisticsSolver.addClause(IVecInt literals) |
IConstr |
DimacsStringSolver.addClause(IVecInt literals) |
IConstr |
SolverDecorator.addClause(IVecInt literals) |
IConstr |
GroupClauseSelectorSolver.addClause(IVecInt literals,
int desc) |
IConstr |
FullClauseSelectorSolver.addControlableClause(IVecInt literals) |
IConstr |
GroupClauseSelectorSolver.addControlableClause(IVecInt literals,
int desc) |
IConstr |
NegationDecorator.addExactly(IVecInt literals,
int n) |
IConstr |
ManyCore.addExactly(IVecInt literals,
int n) |
IConstr |
ClausalCardinalitiesDecorator.addExactly(IVecInt literals,
int k) |
IConstr |
DimacsOutputSolver.addExactly(IVecInt literals,
int n) |
IConstr |
StatisticsSolver.addExactly(IVecInt literals,
int n) |
IConstr |
DimacsStringSolver.addExactly(IVecInt literals,
int n) |
IConstr |
SolverDecorator.addExactly(IVecInt literals,
int n) |
void |
GateTranslator.additionalFullAdderConstraints(int xcarry,
int xsum,
int a,
int b,
int c) |
IConstr |
FullClauseSelectorSolver.addNonControlableClause(IVecInt literals) |
IConstr |
GroupClauseSelectorSolver.addNonControlableClause(IVecInt literals) |
IConstr[] |
GateTranslator.and(int y,
int x1,
int x2)
Translate y <=> x1 /\ x2
|
IConstr[] |
GateTranslator.and(int y,
IVecInt literals)
Translate y <=> x1 /\ x2 /\ ... /\ xn into clauses.
|
void |
LexicoDecorator.discard() |
void |
LexicoDecorator.discardCurrentSolution() |
protected IConstr |
LexicoDecorator.discardSolutionsForOptimizing() |
protected void |
LexicoDecorator.fixCriterionValue() |
void |
LexicoDecorator.forceObjectiveValueTo(Number forcedValue) |
void |
GateTranslator.fullAdderCarry(int x,
int a,
int b,
int c) |
void |
GateTranslator.fullAdderSum(int x,
int a,
int b,
int c) |
IConstr |
GateTranslator.gateFalse(int y)
translate y <=> FALSE into a clause.
|
IConstr |
GateTranslator.gateTrue(int y)
translate y <=> TRUE into a clause.
|
void |
GateTranslator.halfAdderCarry(int x,
int a,
int b) |
void |
GateTranslator.halfAdderSum(int x,
int a,
int b) |
IConstr[] |
GateTranslator.halfOr(int y,
IVecInt literals)
translate y <= x1 \/ x2 \/ ... \/ xn into clauses.
|
protected boolean |
DimacsArrayReader.handleConstr(int gateType,
int output,
int[] inputs) |
protected boolean |
ExtendedDimacsArrayReader.handleConstr(int gateType,
int output,
int[] inputs)
Handles a single constraint (constraint == Extended Dimacs circuit gate).
|
IConstr[] |
GateTranslator.iff(int y,
IVecInt literals)
translate y <=> (x1 <=> x2 <=> ... <=> xn) into clauses.
|
IConstr[] |
GateTranslator.ite(int y,
int x1,
int x2,
int x3)
translate y <=> if x1 then x2 else x3 into clauses.
|
IConstr[] |
GateTranslator.not(int y,
int x)
Translate y <=> not x into clauses.
|
void |
GateTranslator.optimisationFunction(IVecInt literals,
IVec<BigInteger> coefs,
IVecInt result)
Translate an optimization function into constraints and provides the
binary literals in results.
|
IConstr[] |
GateTranslator.or(int y,
IVecInt literals)
translate y <=> x1 \/ x2 \/ ... \/ xn into clauses.
|
ISolver |
DimacsArrayReader.parseInstance(int[] gateType,
int[] outputs,
int[][] inputs,
int maxVar) |
void |
GateTranslator.xor(int x,
int a,
int b) |
IConstr[] |
GateTranslator.xor(int y,
IVecInt literals)
translate y <=> x1 xor x2 xor ... xor xn into clauses.
|
| Modifier and Type | Method and Description |
|---|---|
IConstr |
Policy.addAtLeast(ISolver solver,
IVecInt literals,
int n) |
IConstr |
EncodingStrategyAdapter.addAtLeast(ISolver solver,
IVecInt literals,
int degree) |
IConstr |
EncodingStrategyAdapter.addAtLeastOne(ISolver solver,
IVecInt literals) |
IConstr |
Sequential.addAtMost(ISolver solver,
IVecInt literals,
int k)
This encoding adds (n-1)*k variables (n is the number of variables in the
at most constraint and k is the degree of the constraint) and 2nk+n-3k-1
clauses.
|
IConstr |
Policy.addAtMost(ISolver solver,
IVecInt literals,
int k) |
IConstr |
EncodingStrategyAdapter.addAtMost(ISolver solver,
IVecInt literals,
int degree) |
IConstr |
Product.addAtMost(ISolver solver,
IVecInt literals,
int k) |
IConstr |
Commander.addAtMost(ISolver solver,
IVecInt literals,
int degree) |
IConstr |
Binary.addAtMost(ISolver solver,
IVecInt literals,
int k) |
IConstr |
Binomial.addAtMost(ISolver solver,
IVecInt literals,
int degree) |
IConstr |
Product.addAtMostNonOpt(ISolver solver,
IVecInt literals,
int k) |
IConstr |
Sequential.addAtMostOne(ISolver solver,
IVecInt literals) |
IConstr |
Ladder.addAtMostOne(ISolver solver,
IVecInt literals) |
IConstr |
EncodingStrategyAdapter.addAtMostOne(ISolver solver,
IVecInt literals) |
IConstr |
Product.addAtMostOne(ISolver solver,
IVecInt literals) |
IConstr |
Commander.addAtMostOne(ISolver solver,
IVecInt literals)
In this encoding, variables are partitioned in groups.
|
IConstr |
Binary.addAtMostOne(ISolver solver,
IVecInt literals)
p being the smaller integer greater than log_2(n), this encoding adds p
variables and n*p clauses.
|
IConstr |
Binomial.addAtMostOne(ISolver solver,
IVecInt literals) |
IConstr |
Sequential.addExactly(ISolver solver,
IVecInt literals,
int degree) |
IConstr |
Policy.addExactly(ISolver solver,
IVecInt literals,
int n) |
IConstr |
EncodingStrategyAdapter.addExactly(ISolver solver,
IVecInt literals,
int degree) |
IConstr |
Product.addExactly(ISolver solver,
IVecInt literals,
int degree) |
IConstr |
Commander.addExactly(ISolver solver,
IVecInt literals,
int degree) |
IConstr |
Binary.addExactly(ISolver solver,
IVecInt literals,
int degree) |
IConstr |
Binomial.addExactly(ISolver solver,
IVecInt literals,
int degree) |
IConstr |
Sequential.addExactlyOne(ISolver solver,
IVecInt literals) |
IConstr |
Ladder.addExactlyOne(ISolver solver,
IVecInt literals) |
IConstr |
EncodingStrategyAdapter.addExactlyOne(ISolver solver,
IVecInt literals) |
IConstr |
Product.addExactlyOne(ISolver solver,
IVecInt literals) |
IConstr |
Commander.addExactlyOne(ISolver solver,
IVecInt literals) |
IConstr |
Binary.addExactlyOne(ISolver solver,
IVecInt literals) |
IConstr |
Binomial.addExactlyOne(ISolver solver,
IVecInt literals) |
| Modifier and Type | Method and Description |
|---|---|
IConstr |
Xplain.addAtLeast(IVecInt literals,
int degree) |
IConstr |
HighLevelXplain.addAtLeast(IVecInt literals,
int degree) |
IConstr |
Xplain.addAtMost(IVecInt literals,
int degree) |
IConstr |
HighLevelXplain.addAtMost(IVecInt literals,
int degree) |
IConstr |
Xplain.addExactly(IVecInt literals,
int n) |
Copyright © 2013 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.