| Package | Description |
|---|---|
| org.sat4j |
Contains a command line launcher for the SAT solvers.
|
| org.sat4j.csp |
Classes needed for CSP to SAT translation.
|
| org.sat4j.csp.constraints |
Classes needed for CSP to SAT translation.
|
| org.sat4j.csp.encodings | |
| org.sat4j.maxsat |
MAXSAT and Weighted Max SAT framework.
|
| org.sat4j.maxsat.reader |
Some utility classes to read problems from plain text files.
|
| 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.pb |
Implementations of pseudo boolean solvers
|
| org.sat4j.pb.constraints |
Implementation of data structures for pseudo boolean constraints.
|
| org.sat4j.pb.constraints.pb |
Implementations of pseudo boolean constraints.
|
| org.sat4j.pb.core |
Implementations of pseudo boolean solvers
|
| org.sat4j.pb.reader |
Readers for opb instances.
|
| org.sat4j.pb.tools |
Implementation of different tools for pseudo boolean solvers
|
| org.sat4j.reader |
Some utility classes to read problems from plain text files.
|
| org.sat4j.sat |
Implementation of a sat4j Launcher.
|
| 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 |
|---|---|
void |
Encoding.onFinish(ISolver solver,
IVec<Var> scope) |
void |
Encoding.onNogood(ISolver solver,
IVec<Var> scope,
Map<Evaluable,Integer> tuple) |
void |
Encoding.onSupport(ISolver solver,
IVec<Var> scope,
Map<Evaluable,Integer> tuple) |
void |
Var.toClause(ISolver solver) |
void |
Constant.toClause(ISolver solver) |
void |
Evaluable.toClause(ISolver solver)
Translates a variable over a domain into a set a clauses enforcing that
exactly one value must be chosen in the domain.
|
void |
Predicate.toClause(ISolver solver,
IVec<Var> vscope,
IVec<Evaluable> vars) |
void |
Clausifiable.toClause(ISolver solver,
IVec<Var> scope,
IVec<Evaluable> vars) |
| Modifier and Type | Method and Description |
|---|---|
void |
Nogoods.toClause(ISolver solver,
IVec<Var> scope,
IVec<Evaluable> vars) |
void |
AllDiff.toClause(ISolver solver,
IVec<Var> scope,
IVec<Evaluable> vars) |
void |
AllDiffCard.toClause(ISolver solver,
IVec<Var> scope,
IVec<Evaluable> vars) |
void |
Supports.toClause(ISolver solver,
IVec<Var> scope,
IVec<Evaluable> vars) |
| Modifier and Type | Method and Description |
|---|---|
void |
GeneralizedSupportEncoding.onFinish(ISolver solver,
IVec<Var> scope) |
void |
BinarySupportEncoding.onFinish(ISolver solver,
IVec<Var> scope) |
void |
GeneralizedSupportEncoding.onNogood(ISolver solver,
IVec<Var> scope,
Map<Evaluable,Integer> tuple) |
void |
BinarySupportEncoding.onNogood(ISolver solver,
IVec<Var> scope,
Map<Evaluable,Integer> tuple) |
void |
DirectEncoding.onNogood(ISolver solver,
IVec<Var> scope,
Map<Evaluable,Integer> tuple) |
void |
GeneralizedSupportEncoding.onSupport(ISolver solver,
IVec<Var> scope,
Map<Evaluable,Integer> tuple) |
void |
BinarySupportEncoding.onSupport(ISolver solver,
IVec<Var> scope,
Map<Evaluable,Integer> tuple) |
| Modifier and Type | Method and Description |
|---|---|
IConstr |
WeightedMaxSatDecorator.addClause(IVecInt literals)
Add a soft clause to the solver.
|
IConstr |
WeightedMaxSatDecorator.addHardClause(IVecInt literals)
Add a hard clause in the solver, i.e. a clause that must be satisfied.
|
IConstr |
WeightedMaxSatDecorator.addSoftAtLeast(BigInteger weight,
IVecInt literals,
int degree)
Allow adding a new soft cardinality constraint in the solver.
|
IConstr |
WeightedMaxSatDecorator.addSoftAtLeast(int weight,
IVecInt literals,
int degree)
Allow adding a new soft cardinality constraint in the solver.
|
IConstr |
WeightedMaxSatDecorator.addSoftAtLeast(IVecInt literals,
int degree)
Allow adding a new soft cardinality constraint in the solver.
|
IConstr |
WeightedMaxSatDecorator.addSoftAtMost(BigInteger weight,
IVecInt literals,
int degree)
Allow adding a new soft cardinality constraint in the solver.
|
IConstr |
WeightedMaxSatDecorator.addSoftAtMost(int weight,
IVecInt literals,
int degree)
Allow adding a new soft cardinality constraint in the solver.
|
IConstr |
WeightedMaxSatDecorator.addSoftAtMost(IVecInt literals,
int degree)
Allow adding a new soft cardinality constraint in the solver.
|
IConstr |
WeightedMaxSatDecorator.addSoftClause(BigInteger weight,
IVecInt literals) |
IConstr |
WeightedMaxSatDecorator.addSoftClause(int weight,
IVecInt literals)
Add a soft clause to the solver.
|
IConstr |
WeightedMaxSatDecorator.addSoftClause(IVecInt literals)
Add a soft clause in the solver, i.e. a clause with a weight of 1.
|
void |
MinCostDecorator.discard() |
void |
MinCostDecorator.discardCurrentSolution() |
void |
WeightedMaxSatDecorator.forceObjectiveValueTo(Number forcedValue)
Force the solver to find a solution with a specific value (nice to find
all optimal solutions for instance).
|
void |
MinCostDecorator.forceObjectiveValueTo(Number forcedValue) |
protected IProblem |
GenericOptLauncher.readProblem(String problemname) |
| Modifier and Type | Method and Description |
|---|---|
protected void |
WDimacsReader.flushConstraint() |
protected boolean |
WDimacsReader.handleLine() |
| 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 |
|---|---|
IConstr |
UserFriendlyPBStringSolver.addAtLeast(IVecInt literals,
int degree) |
IConstr |
LPStringSolver.addAtLeast(IVecInt literals,
int degree) |
IConstr |
OPBStringSolver.addAtLeast(IVecInt literals,
int degree) |
IConstr |
PseudoBitsAdderDecorator.addAtLeast(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree) |
IConstr |
IPBSolver.addAtLeast(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree)
Create a pseudo-boolean constraint of the type "at least".
|
IConstr |
UserFriendlyPBStringSolver.addAtLeast(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree) |
IConstr |
LPStringSolver.addAtLeast(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree) |
IConstr |
PBSolverDecorator.addAtLeast(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree) |
IConstr |
OPBStringSolver.addAtLeast(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree) |
IConstr |
PseudoBitsAdderDecorator.addAtLeast(IVecInt literals,
IVecInt coeffs,
int degree) |
IConstr |
IPBSolver.addAtLeast(IVecInt literals,
IVecInt coeffs,
int degree)
Create a pseudo-boolean constraint of the type "at least".
|
IConstr |
UserFriendlyPBStringSolver.addAtLeast(IVecInt literals,
IVecInt coeffs,
int degree) |
IConstr |
LPStringSolver.addAtLeast(IVecInt literals,
IVecInt coeffs,
int degree) |
IConstr |
PBSolverDecorator.addAtLeast(IVecInt literals,
IVecInt coeffs,
int degree) |
IConstr |
OPBStringSolver.addAtLeast(IVecInt literals,
IVecInt coeffs,
int degree) |
IConstr |
UserFriendlyPBStringSolver.addAtMost(IVecInt literals,
int degree) |
IConstr |
LPStringSolver.addAtMost(IVecInt literals,
int degree) |
IConstr |
OPBStringSolver.addAtMost(IVecInt literals,
int degree) |
IConstr |
PseudoBitsAdderDecorator.addAtMost(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree) |
IConstr |
IPBSolver.addAtMost(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree)
Create a pseudo boolean constraint of the type "at most".
|
IConstr |
UserFriendlyPBStringSolver.addAtMost(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree) |
IConstr |
LPStringSolver.addAtMost(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree) |
IConstr |
PBSolverDecorator.addAtMost(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree) |
IConstr |
OPBStringSolver.addAtMost(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree) |
IConstr |
PseudoBitsAdderDecorator.addAtMost(IVecInt literals,
IVecInt coeffs,
int degree) |
IConstr |
IPBSolver.addAtMost(IVecInt literals,
IVecInt coeffs,
int degree)
Create a pseudo boolean constraint of the type "at most".
|
IConstr |
UserFriendlyPBStringSolver.addAtMost(IVecInt literals,
IVecInt coeffs,
int degree) |
IConstr |
LPStringSolver.addAtMost(IVecInt literals,
IVecInt coeffs,
int degree) |
IConstr |
PBSolverDecorator.addAtMost(IVecInt literals,
IVecInt coeffs,
int degree) |
IConstr |
OPBStringSolver.addAtMost(IVecInt literals,
IVecInt coeffs,
int degree) |
IConstr |
UserFriendlyPBStringSolver.addClause(IVecInt literals) |
IConstr |
LPStringSolver.addClause(IVecInt literals) |
IConstr |
OPBStringSolver.addClause(IVecInt literals) |
IConstr |
OPBStringSolver.addExactly(IVecInt literals,
int weight) |
IConstr |
PseudoBitsAdderDecorator.addExactly(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger weight) |
IConstr |
IPBSolver.addExactly(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger weight)
Create a pseudo-boolean constraint of the type "subset sum".
|
IConstr |
UserFriendlyPBStringSolver.addExactly(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger weight) |
IConstr |
LPStringSolver.addExactly(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger weight) |
IConstr |
PBSolverDecorator.addExactly(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger weight) |
IConstr |
OPBStringSolver.addExactly(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger weight) |
IConstr |
PseudoBitsAdderDecorator.addExactly(IVecInt literals,
IVecInt coeffs,
int weight) |
IConstr |
IPBSolver.addExactly(IVecInt literals,
IVecInt coeffs,
int weight)
Create a pseudo-boolean constraint of the type "subset sum".
|
IConstr |
UserFriendlyPBStringSolver.addExactly(IVecInt literals,
IVecInt coeffs,
int weight) |
IConstr |
LPStringSolver.addExactly(IVecInt literals,
IVecInt coeffs,
int weight) |
IConstr |
PBSolverDecorator.addExactly(IVecInt literals,
IVecInt coeffs,
int weight) |
IConstr |
OPBStringSolver.addExactly(IVecInt literals,
IVecInt coeffs,
int weight) |
IConstr |
PseudoBitsAdderDecorator.addPseudoBoolean(IVecInt lits,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger d) |
IConstr |
IPBSolver.addPseudoBoolean(IVecInt lits,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger d)
Create a Pseudo-Boolean constraint of the type "at least n or at most n
of those literals must be satisfied"
|
IConstr |
UserFriendlyPBStringSolver.addPseudoBoolean(IVecInt lits,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger d) |
IConstr |
LPStringSolver.addPseudoBoolean(IVecInt lits,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger d) |
IConstr |
PBSolverDecorator.addPseudoBoolean(IVecInt lits,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger d) |
IConstr |
OPBStringSolver.addPseudoBoolean(IVecInt lits,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger d) |
void |
PseudoOptDecorator.discard() |
void |
PseudoOptDecorator.discardCurrentSolution() |
void |
PseudoIteratorDecorator.discardCurrentSolution() |
void |
ConstraintRelaxingPseudoOptDecorator.forceObjectiveValueTo(Number forcedValue) |
void |
PseudoOptDecorator.forceObjectiveValueTo(Number forcedValue) |
protected IProblem |
LanceurPseudo2005.readProblem(String problemname) |
| Modifier and Type | Method and Description |
|---|---|
protected abstract Constr |
AbstractPBDataStructureFactory.constraintFactory(int[] literals,
BigInteger[] coefs,
BigInteger degree) |
protected Constr |
AbstractPBClauseCardConstrDataStructure.constraintFactory(int[] literals,
BigInteger[] coefs,
BigInteger degree) |
protected PBConstr |
PuebloPBMinDataStructure.constraintFactory(int[] literals,
BigInteger[] coefs,
BigInteger degree) |
protected PBConstr |
PBMinDataStructure.constraintFactory(int[] literals,
BigInteger[] coefs,
BigInteger degree) |
protected Constr |
PBMaxDataStructure.constraintFactory(int[] literals,
BigInteger[] coefs,
BigInteger degree) |
protected Constr |
AbstractPBClauseCardConstrDataStructure.constructCard(IVecInt theLits,
int degree) |
Constr |
MinCardConstructor.constructCard(UnitPropagationListener solver,
ILits voc,
IVecInt theLits,
int degree) |
Constr |
ICardConstructor.constructCard(UnitPropagationListener solver,
ILits voc,
IVecInt theLits,
int degree) |
Constr |
AtLeastCardPBConstructor.constructCard(UnitPropagationListener solver,
ILits voc,
IVecInt theLits,
int degree) |
Constr |
MinCardPBConstructor.constructCard(UnitPropagationListener solver,
ILits voc,
IVecInt theLits,
int degree) |
Constr |
AtLeastCardConstructor.constructCard(UnitPropagationListener solver,
ILits voc,
IVecInt theLits,
int degree) |
protected Constr |
AbstractPBClauseCardConstrDataStructure.constructPB(int[] theLits,
BigInteger[] coefs,
BigInteger degree) |
Constr |
MinLongWatchPBConstructor.constructPB(UnitPropagationListener solver,
ILits voc,
int[] theLits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs) |
Constr |
MaxLongWatchPBConstructor.constructPB(UnitPropagationListener solver,
ILits voc,
int[] theLits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs) |
Constr |
MinWatchPBConstructor.constructPB(UnitPropagationListener solver,
ILits voc,
int[] theLits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs) |
Constr |
MaxWatchPBConstructor.constructPB(UnitPropagationListener solver,
ILits voc,
int[] theLits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs) |
Constr |
MinLongWatchPBCPConstructor.constructPB(UnitPropagationListener solver,
ILits voc,
int[] theLits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs) |
Constr |
MaxLongWatchPBCPConstructor.constructPB(UnitPropagationListener solver,
ILits voc,
int[] theLits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs) |
Constr |
IPBConstructor.constructPB(UnitPropagationListener solver,
ILits voc,
int[] theLits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs) |
Constr |
PuebloMinWatchPBConstructor.constructPB(UnitPropagationListener solver,
ILits voc,
int[] theLits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs) |
Constr |
AbstractPBDataStructureFactory.createAtLeastPBConstraint(IVecInt literals,
IVec<BigInteger> coefs,
BigInteger degree) |
Constr |
AbstractPBDataStructureFactory.createAtMostPBConstraint(IVecInt literals,
IVec<BigInteger> coefs,
BigInteger degree) |
Constr |
AbstractPBDataStructureFactory.createCardinalityConstraint(IVecInt literals,
int degree) |
Constr |
AbstractPBDataStructureFactory.createClause(IVecInt literals) |
Constr |
AbstractPBClauseCardConstrDataStructure.createClause(IVecInt literals) |
Constr |
PuebloPBMinClauseCardConstrDataStructure.createClause(IVecInt literals) |
Constr |
AbstractPBDataStructureFactory.createPseudoBooleanConstraint(IVecInt literals,
IVec<BigInteger> coefs,
boolean moreThan,
BigInteger degree) |
| Modifier and Type | Method and Description |
|---|---|
static PBConstr |
AtLeastPB.atLeastNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
int n) |
protected void |
MaxWatchPb.computePropagation(UnitPropagationListener s) |
protected void |
MinWatchPbLong.computePropagation(UnitPropagationListener s) |
protected abstract void |
WatchPbLongCP.computePropagation(UnitPropagationListener s) |
protected abstract void |
WatchPb.computePropagation(UnitPropagationListener s) |
protected void |
MaxWatchPbLongCP.computePropagation(UnitPropagationListener s) |
protected void |
MinWatchPb.computePropagation(UnitPropagationListener s) |
protected abstract void |
WatchPbLong.computePropagation(UnitPropagationListener s) |
protected void |
MinWatchPbLongCP.computePropagation(UnitPropagationListener s) |
protected void |
MaxWatchPbLong.computePropagation(UnitPropagationListener s) |
protected void |
MaxWatchPb.computeWatches()
All the literals are watched.
|
protected void |
MinWatchPbLong.computeWatches() |
protected abstract void |
WatchPbLongCP.computeWatches() |
protected abstract void |
WatchPb.computeWatches() |
protected void |
MaxWatchPbLongCP.computeWatches()
All the literals are watched.
|
protected void |
MinWatchPb.computeWatches() |
protected abstract void |
WatchPbLong.computeWatches() |
protected void |
MinWatchPbLongCP.computeWatches() |
protected void |
MaxWatchPbLong.computeWatches()
All the literals are watched.
|
static PBConstr |
MinWatchCardPB.minWatchCardPBNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
boolean moreThan,
int degree)
Permet la cr?
|
static IDataStructurePB |
Pseudos.niceParameters(IVecInt ps,
IVec<BigInteger> bigCoefs,
boolean moreThan,
BigInteger bigDeg,
ILits voc) |
static BigInteger |
Pseudos.niceParametersForCompetition(int[] ps,
BigInteger[] bigCoefs,
boolean moreThan,
BigInteger bigDeg) |
static MaxWatchPb |
MaxWatchPb.normalizedMaxWatchPbNew(UnitPropagationListener s,
ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs)
build a pseudo boolean constraint.
|
static MaxWatchPbLongCP |
MaxWatchPbLongCP.normalizedMaxWatchPbNew(UnitPropagationListener s,
ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs)
build a pseudo boolean constraint.
|
static MaxWatchPbLong |
MaxWatchPbLong.normalizedMaxWatchPbNew(UnitPropagationListener s,
ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs)
build a pseudo boolean constraint.
|
static PBConstr |
MinWatchCardPB.normalizedMinWatchCardPBNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
int degree)
Permet la cr?
|
static PuebloMinWatchPb |
PuebloMinWatchPb.normalizedMinWatchPbNew(UnitPropagationListener s,
ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree) |
static MinWatchPbLong |
MinWatchPbLong.normalizedMinWatchPbNew(UnitPropagationListener s,
ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs)
build a pseudo boolean constraint.
|
static MinWatchPb |
MinWatchPb.normalizedMinWatchPbNew(UnitPropagationListener s,
ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs)
build a pseudo boolean constraint.
|
static MinWatchPbLongCP |
MinWatchPbLongCP.normalizedMinWatchPbNew(UnitPropagationListener s,
ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs)
build a pseudo boolean constraint.
|
| Modifier and Type | Method and Description |
|---|---|
void |
ObjectiveReducerPBSolverDecorator.addAllClauses(IVec<IVecInt> clauses) |
IConstr |
ObjectiveReducerPBSolverDecorator.addAtLeast(IVecInt literals,
int degree) |
IConstr |
PBSolver.addAtLeast(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree) |
IConstr |
ObjectiveReducerPBSolverDecorator.addAtLeast(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree) |
IConstr |
PBSolver.addAtLeast(IVecInt literals,
IVecInt coeffs,
int degree) |
IConstr |
ObjectiveReducerPBSolverDecorator.addAtLeast(IVecInt literals,
IVecInt coeffs,
int degree) |
IConstr |
ObjectiveReducerPBSolverDecorator.addAtMost(IVecInt literals,
int degree) |
IConstr |
PBSolver.addAtMost(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree) |
IConstr |
ObjectiveReducerPBSolverDecorator.addAtMost(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree) |
IConstr |
PBSolver.addAtMost(IVecInt literals,
IVecInt coeffs,
int degree) |
IConstr |
ObjectiveReducerPBSolverDecorator.addAtMost(IVecInt literals,
IVecInt coeffs,
int degree) |
IConstr |
ObjectiveReducerPBSolverDecorator.addBlockingClause(IVecInt literals) |
IConstr |
ObjectiveReducerPBSolverDecorator.addClause(IVecInt literals) |
IConstr |
ObjectiveReducerPBSolverDecorator.addExactly(IVecInt literals,
int n) |
IConstr |
PBSolver.addExactly(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger weight) |
IConstr |
ObjectiveReducerPBSolverDecorator.addExactly(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger weight) |
IConstr |
PBSolver.addExactly(IVecInt literals,
IVecInt coeffs,
int weight) |
IConstr |
ObjectiveReducerPBSolverDecorator.addExactly(IVecInt literals,
IVecInt coeffs,
int weight) |
IConstr |
PBSolver.addPseudoBoolean(IVecInt literals,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger degree) |
IConstr |
PBSolverWithImpliedClause.addPseudoBoolean(IVecInt literals,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger degree) |
IConstr |
ObjectiveReducerPBSolverDecorator.addPseudoBoolean(IVecInt lits,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger d) |
Constr |
PBDataStructureFactory.createAtLeastPBConstraint(IVecInt literals,
IVec<BigInteger> coefs,
BigInteger degree) |
Constr |
PBDataStructureFactory.createAtMostPBConstraint(IVecInt literals,
IVec<BigInteger> coefs,
BigInteger degree) |
Constr |
PBDataStructureFactory.createPseudoBooleanConstraint(IVecInt literals,
IVec<BigInteger> coefs,
boolean moreThan,
BigInteger degree) |
| Modifier and Type | Method and Description |
|---|---|
protected void |
OPBReader2005.endConstraint() |
protected void |
OPBReader2010.endConstraint() |
protected void |
JSONPBReader.handleNotHandled(String constraint) |
void |
OPBReader2005.parse()
parses the file and uses the callbacks to send to send the data back to
the program
|
IProblem |
OPBReader2005.parseInstance(InputStream in) |
protected IProblem |
OPBReader2005.parseInstance(LineNumberReader input) |
IProblem |
OPBReader2012.parseInstance(Reader input) |
IProblem |
OPBReader2005.parseInstance(Reader input) |
IProblem |
OPBReader2010.parseInstance(Reader input) |
protected void |
OPBReader2005.readConstraint()
read a constraint calls beginConstraint, constraintTerm and endConstraint
|
| Modifier and Type | Method and Description |
|---|---|
IConstr |
XplainPB.addAtLeast(IVecInt literals,
int degree) |
IConstr |
PBAdapter.addAtLeast(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree) |
IConstr |
ClausalConstraintsDecorator.addAtLeast(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree) |
IConstr |
XplainPB.addAtLeast(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree) |
IConstr |
ManyCorePB.addAtLeast(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree) |
IConstr |
LexicoDecoratorPB.addAtLeast(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree) |
IConstr |
PBAdapter.addAtLeast(IVecInt literals,
IVecInt coeffs,
int degree) |
IConstr |
ClausalConstraintsDecorator.addAtLeast(IVecInt literals,
IVecInt coeffs,
int degree) |
IConstr |
XplainPB.addAtLeast(IVecInt literals,
IVecInt coeffs,
int degree) |
IConstr |
ManyCorePB.addAtLeast(IVecInt literals,
IVecInt coeffs,
int degree) |
IConstr |
LexicoDecoratorPB.addAtLeast(IVecInt literals,
IVecInt coeffs,
int degree) |
IConstr |
XplainPB.addAtMost(IVecInt literals,
int degree) |
IConstr |
PBAdapter.addAtMost(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree) |
IConstr |
ClausalConstraintsDecorator.addAtMost(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree) |
IConstr |
XplainPB.addAtMost(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree) |
IConstr |
ManyCorePB.addAtMost(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree) |
IConstr |
LexicoDecoratorPB.addAtMost(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree) |
IConstr |
PBAdapter.addAtMost(IVecInt literals,
IVecInt coeffs,
int degree) |
IConstr |
ClausalConstraintsDecorator.addAtMost(IVecInt literals,
IVecInt coeffs,
int degree) |
IConstr |
XplainPB.addAtMost(IVecInt literals,
IVecInt coeffs,
int degree) |
IConstr |
ManyCorePB.addAtMost(IVecInt literals,
IVecInt coeffs,
int degree) |
IConstr |
LexicoDecoratorPB.addAtMost(IVecInt literals,
IVecInt coeffs,
int degree) |
IConstr |
XplainPB.addExactly(IVecInt literals,
int n) |
IConstr |
PBAdapter.addExactly(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger weight) |
IConstr |
ClausalConstraintsDecorator.addExactly(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger weight) |
IConstr |
XplainPB.addExactly(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger weight) |
IConstr |
ManyCorePB.addExactly(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger weight) |
IConstr |
LexicoDecoratorPB.addExactly(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger weight) |
IConstr |
PBAdapter.addExactly(IVecInt literals,
IVecInt coeffs,
int weight) |
IConstr |
ClausalConstraintsDecorator.addExactly(IVecInt literals,
IVecInt coeffs,
int weight) |
IConstr |
XplainPB.addExactly(IVecInt literals,
IVecInt coeffs,
int weight) |
IConstr |
ManyCorePB.addExactly(IVecInt literals,
IVecInt coeffs,
int weight) |
IConstr |
LexicoDecoratorPB.addExactly(IVecInt literals,
IVecInt coeffs,
int weight) |
IConstr |
PBAdapter.addPseudoBoolean(IVecInt lits,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger d) |
IConstr |
ClausalConstraintsDecorator.addPseudoBoolean(IVecInt lits,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger d) |
IConstr |
XplainPB.addPseudoBoolean(IVecInt lits,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger d) |
IConstr |
ManyCorePB.addPseudoBoolean(IVecInt lits,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger d) |
IConstr |
LexicoDecoratorPB.addPseudoBoolean(IVecInt lits,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger d) |
void |
DependencyHelper.and(C name,
T thing,
T... otherThings)
Create a constraint of the form thing <=> (thing1 and thing 2 ... and
thingn)
|
ImplicationAnd<T,C> |
ImplicationAnd.and(T thing)
Add a new positive literal to the conjunction of literals.
|
ImplicationAnd<T,C> |
ImplicationAnd.andNot(T thing)
Add a new negative literal to the conjunction of literals.
|
void |
DependencyHelper.atLeast(C name,
BigInteger degree,
WeightedObject<T>... wobj)
Create a PB constraint of the form
w1.l1 + w2.l2 + ... wn.ln >= degree
where wi are position integers and li are domain objects. |
void |
DependencyHelper.atLeast(C name,
int i,
T... things)
Create a constraint stating that at most i domain object should be set to
true.
|
void |
DependencyHelper.atMost(C name,
BigInteger degree,
WeightedObject<T>... wobj)
Create a PB constraint of the form
w1.l1 + w2.l2 + ... wn.ln <= degree
where wi are position integers and li are domain objects. |
void |
DependencyHelper.atMost(C name,
int i,
T... things)
Create a constraint stating that at most i domain object should be set to
true.
|
void |
DependencyHelper.atMost(C name,
int degree,
WeightedObject<T>... wobj) |
ImplicationNamer<T,C> |
DependencyHelper.atMost(int i,
T... things)
Create a constraint stating that at most i domain object should be set to
true.
|
void |
DependencyHelper.clause(C name,
T... things)
Create a clause (thing1 or thing 2 ... or thingn)
|
void |
DependencyHelper.discard(IVec<T> things) |
protected IConstr |
LexicoDecoratorPB.discardSolutionsForOptimizing() |
void |
DependencyHelper.discardSolutionsWithObjectiveValueGreaterThan(long value) |
protected void |
LexicoDecoratorPB.fixCriterionValue() |
void |
DependencyHelper.halfOr(C name,
T thing,
T... otherThings)
Create a constraint of the form thing <= (thing1 or thing 2 ... or
thingn)
|
void |
DependencyHelper.iff(C name,
T thing,
T... otherThings)
Create a constraint using equivalency chains thing <=> (thing1 <=> thing2
<=> ... <=> thingn)
|
void |
DependencyHelper.ifThenElse(C name,
T thing,
T conditionThing,
T thenThing,
T elseThing)
Create a constraint of the form thing <=> (if conditionThing then
thenThing else elseThing)
|
ImplicationNamer<T,C> |
DisjunctionRHS.implies(T... things) |
ImplicationNamer<T,C> |
ImplicationRHS.implies(T... things)
Build an implication with a disjunction of literals in the RHS.
|
ImplicationAnd<T,C> |
ImplicationRHS.implies(T thing)
Build an implication with a conjunction of literals in the RHS.
|
ImplicationAnd<T,C> |
ImplicationRHS.impliesNot(T thing)
Build an implication with a conjunction of literals in the RHS.
|
void |
DependencyHelper.or(C name,
T thing,
T... otherThings)
Create a constraint of the form thing <=> (thing1 or thing 2 ... or
thingn)
|
void |
DependencyHelper.setFalse(T thing,
C name)
Add a constraint to set the value of a domain object to false.
|
void |
DependencyHelper.setTrue(T thing,
C name)
Add a constraint to set the value of a domain object to true.
|
| 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 |
CSPReader.parseInstance(InputStream in) |
IProblem |
XMLCSPReader.parseInstance(InputStream in) |
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 |
CSPReader.parseInstance(Reader in) |
IProblem |
CSPInstanceReader.parseInstance(Reader in) |
IProblem |
XMLCSPReader.parseInstance(Reader in) |
IProblem |
Reader.parseInstance(Reader in)
Deprecated.
|
IProblem |
CSPInstanceReader.parseInstance(String filename) |
IProblem |
XMLCSPReader.parseInstance(String filename) |
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 |
|---|---|
protected IProblem |
Lanceur.readProblem(String problemname)
Deprecated.
|
| 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.