|
||||||||||
| PREV NEXT | FRAMES NO FRAMES | |||||||||
| Packages that use ContradictionException | |
|---|---|
| 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. |
| Uses of ContradictionException in org.sat4j |
|---|
| Methods in org.sat4j that throw ContradictionException | |
|---|---|
protected IProblem |
AbstractLauncher.readProblem(String problemname)
Reads a problem file from the command line. |
| Uses of ContradictionException in org.sat4j.csp |
|---|
| Methods in org.sat4j.csp that throw ContradictionException | |
|---|---|
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 |
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 |
Constant.toClause(ISolver solver)
|
void |
Predicate.toClause(ISolver solver,
IVec<Var> vscope,
IVec<Evaluable> vars)
|
void |
Clausifiable.toClause(ISolver solver,
IVec<Var> scope,
IVec<Evaluable> vars)
|
| Uses of ContradictionException in org.sat4j.csp.constraints |
|---|
| Methods in org.sat4j.csp.constraints that throw ContradictionException | |
|---|---|
void |
Supports.toClause(ISolver solver,
IVec<Var> scope,
IVec<Evaluable> vars)
|
void |
Nogoods.toClause(ISolver solver,
IVec<Var> scope,
IVec<Evaluable> vars)
|
void |
AllDiff.toClause(ISolver solver,
IVec<Var> scope,
IVec<Evaluable> vars)
|
| Uses of ContradictionException in org.sat4j.csp.encodings |
|---|
| Methods in org.sat4j.csp.encodings that throw ContradictionException | |
|---|---|
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 |
DirectEncoding.onNogood(ISolver solver,
IVec<Var> scope,
Map<Evaluable,Integer> tuple)
|
void |
BinarySupportEncoding.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)
|
| Uses of ContradictionException in org.sat4j.maxsat |
|---|
| Methods in org.sat4j.maxsat that throw ContradictionException | |
|---|---|
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)
|
| Uses of ContradictionException in org.sat4j.maxsat.reader |
|---|
| Methods in org.sat4j.maxsat.reader that throw ContradictionException | |
|---|---|
protected void |
WDimacsReader.flushConstraint()
|
protected boolean |
WDimacsReader.handleLine()
|
| Uses of ContradictionException in org.sat4j.minisat.constraints |
|---|
| Methods in org.sat4j.minisat.constraints that throw ContradictionException | |
|---|---|
Constr |
MixedDataStructureSingleWL.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
MixedDataStructureDanielWL.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
MixedDataStructureDanielHT.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
CardinalityDataStructureYanMin.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
CardinalityDataStructureYanMax.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
CardinalityDataStructure.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
AbstractDataStructureFactory.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
MixedDataStructureSingleWL.createClause(IVecInt literals)
|
Constr |
MixedDataStructureDanielWL.createClause(IVecInt literals)
|
Constr |
MixedDataStructureDanielHT.createClause(IVecInt literals)
|
Constr |
ClausalDataStructureWL.createClause(IVecInt literals)
|
Constr |
CardinalityDataStructureYanMin.createClause(IVecInt literals)
|
Constr |
CardinalityDataStructureYanMax.createClause(IVecInt literals)
|
Constr |
CardinalityDataStructure.createClause(IVecInt literals)
|
| Uses of ContradictionException in org.sat4j.minisat.constraints.card |
|---|
| Methods in org.sat4j.minisat.constraints.card that throw ContradictionException | |
|---|---|
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)
|
| Uses of ContradictionException in org.sat4j.minisat.constraints.cnf |
|---|
| Methods in org.sat4j.minisat.constraints.cnf that throw ContradictionException | |
|---|---|
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 |
| Uses of ContradictionException in org.sat4j.minisat.core |
|---|
| Methods in org.sat4j.minisat.core that throw ContradictionException | |
|---|---|
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)
|
| Uses of ContradictionException in org.sat4j.opt |
|---|
| Methods in org.sat4j.opt that throw ContradictionException | |
|---|---|
IConstr |
MaxSatDecorator.addClause(IVecInt literals)
|
void |
MinOneDecorator.discard()
|
void |
MaxSatDecorator.discard()
|
void |
MinOneDecorator.discardCurrentSolution()
|
void |
MaxSatDecorator.discardCurrentSolution()
|
void |
MinOneDecorator.forceObjectiveValueTo(Number forcedValue)
|
void |
MaxSatDecorator.forceObjectiveValueTo(Number forcedValue)
|
| Uses of ContradictionException in org.sat4j.pb |
|---|
| Methods in org.sat4j.pb that throw ContradictionException | |
|---|---|
IConstr |
UserFriendlyPBStringSolver.addAtLeast(IVecInt literals,
int degree)
|
IConstr |
OPBStringSolver.addAtLeast(IVecInt literals,
int degree)
|
IConstr |
LPStringSolver.addAtLeast(IVecInt literals,
int degree)
|
IConstr |
UserFriendlyPBStringSolver.addAtLeast(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree)
|
IConstr |
PseudoBitsAdderDecorator.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 |
LPStringSolver.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,
IVecInt coeffs,
int degree)
|
IConstr |
PseudoBitsAdderDecorator.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 |
LPStringSolver.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.addAtMost(IVecInt literals,
int degree)
|
IConstr |
OPBStringSolver.addAtMost(IVecInt literals,
int degree)
|
IConstr |
LPStringSolver.addAtMost(IVecInt literals,
int degree)
|
IConstr |
UserFriendlyPBStringSolver.addAtMost(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree)
|
IConstr |
PseudoBitsAdderDecorator.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 |
LPStringSolver.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,
IVecInt coeffs,
int degree)
|
IConstr |
PseudoBitsAdderDecorator.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 |
LPStringSolver.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.addClause(IVecInt literals)
|
IConstr |
OPBStringSolver.addClause(IVecInt literals)
|
IConstr |
LPStringSolver.addClause(IVecInt literals)
|
IConstr |
UserFriendlyPBStringSolver.addExactly(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger weight)
|
IConstr |
PseudoBitsAdderDecorator.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 |
LPStringSolver.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,
IVecInt coeffs,
int weight)
|
IConstr |
PseudoBitsAdderDecorator.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 |
LPStringSolver.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.addPseudoBoolean(IVecInt lits,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger d)
|
IConstr |
PseudoBitsAdderDecorator.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)
|
IConstr |
LPStringSolver.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" |
void |
PseudoOptDecorator.discard()
|
void |
PseudoOptDecorator.discardCurrentSolution()
|
void |
PseudoIteratorDecorator.discardCurrentSolution()
|
void |
PseudoOptDecorator.forceObjectiveValueTo(Number forcedValue)
|
void |
ConstraintRelaxingPseudoOptDecorator.forceObjectiveValueTo(Number forcedValue)
|
protected IProblem |
LanceurPseudo2005.readProblem(String problemname)
|
| Uses of ContradictionException in org.sat4j.pb.constraints |
|---|
| Methods in org.sat4j.pb.constraints that throw ContradictionException | |
|---|---|
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 abstract Constr |
AbstractPBDataStructureFactory.constraintFactory(int[] literals,
BigInteger[] coefs,
BigInteger degree)
|
protected Constr |
AbstractPBClauseCardConstrDataStructure.constraintFactory(int[] literals,
BigInteger[] coefs,
BigInteger degree)
|
protected Constr |
AbstractPBClauseCardConstrDataStructure.constructCard(IVecInt theLits,
int degree)
|
Constr |
MinCardPBConstructor.constructCard(UnitPropagationListener solver,
ILits voc,
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 |
AtLeastCardConstructor.constructCard(UnitPropagationListener solver,
ILits voc,
IVecInt theLits,
int degree)
|
protected Constr |
AbstractPBClauseCardConstrDataStructure.constructPB(int[] theLits,
BigInteger[] coefs,
BigInteger degree)
|
Constr |
PuebloMinWatchPBConstructor.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 |
MinLongWatchPBCPConstructor.constructPB(UnitPropagationListener solver,
ILits voc,
int[] theLits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs)
|
Constr |
MinLongWatchPBConstructor.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 |
MaxLongWatchPBCPConstructor.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 |
IPBConstructor.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 |
PuebloPBMinClauseCardConstrDataStructure.createClause(IVecInt literals)
|
Constr |
AbstractPBDataStructureFactory.createClause(IVecInt literals)
|
Constr |
AbstractPBClauseCardConstrDataStructure.createClause(IVecInt literals)
|
Constr |
AbstractPBDataStructureFactory.createPseudoBooleanConstraint(IVecInt literals,
IVec<BigInteger> coefs,
boolean moreThan,
BigInteger degree)
|
| Uses of ContradictionException in org.sat4j.pb.constraints.pb |
|---|
| Methods in org.sat4j.pb.constraints.pb that throw ContradictionException | |
|---|---|
static PBConstr |
AtLeastPB.atLeastNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
int n)
|
protected abstract void |
WatchPbLongCP.computePropagation(UnitPropagationListener s)
|
protected abstract void |
WatchPbLong.computePropagation(UnitPropagationListener s)
|
protected abstract void |
WatchPb.computePropagation(UnitPropagationListener s)
|
protected void |
MinWatchPbLongLimit.computePropagation(UnitPropagationListener s)
|
protected void |
MinWatchPbLongCP.computePropagation(UnitPropagationListener s)
|
protected void |
MinWatchPbLong.computePropagation(UnitPropagationListener s)
|
protected void |
MinWatchPb.computePropagation(UnitPropagationListener s)
|
protected void |
MaxWatchPbLongCP.computePropagation(UnitPropagationListener s)
|
protected void |
MaxWatchPbLong.computePropagation(UnitPropagationListener s)
|
protected void |
MaxWatchPb.computePropagation(UnitPropagationListener s)
|
protected abstract void |
WatchPbLongCP.computeWatches()
|
protected abstract void |
WatchPbLong.computeWatches()
|
protected abstract void |
WatchPb.computeWatches()
|
protected void |
MinWatchPbLongLimit.computeWatches()
|
protected void |
MinWatchPbLongCP.computeWatches()
|
protected void |
MinWatchPbLong.computeWatches()
|
protected void |
MinWatchPb.computeWatches()
|
protected void |
MaxWatchPbLongCP.computeWatches()
All the literals are watched. |
protected void |
MaxWatchPbLong.computeWatches()
All the literals are watched. |
protected void |
MaxWatchPb.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 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 MaxWatchPb |
MaxWatchPb.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 MinWatchPbLongLimit |
MinWatchPbLongLimit.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. |
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. |
| Uses of ContradictionException in org.sat4j.pb.core |
|---|
| Methods in org.sat4j.pb.core that throw ContradictionException | |
|---|---|
IConstr |
PBSolver.addAtLeast(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree)
|
IConstr |
PBSolver.addAtLeast(IVecInt literals,
IVecInt coeffs,
int degree)
|
IConstr |
PBSolver.addAtMost(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree)
|
IConstr |
PBSolver.addAtMost(IVecInt literals,
IVecInt coeffs,
int degree)
|
IConstr |
PBSolver.addExactly(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger weight)
|
IConstr |
PBSolver.addExactly(IVecInt literals,
IVecInt coeffs,
int weight)
|
IConstr |
PBSolverWithImpliedClause.addPseudoBoolean(IVecInt literals,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger degree)
|
IConstr |
PBSolver.addPseudoBoolean(IVecInt literals,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger degree)
|
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)
|
| Uses of ContradictionException in org.sat4j.pb.reader |
|---|
| Methods in org.sat4j.pb.reader that throw ContradictionException | |
|---|---|
protected void |
OPBReader2010.endConstraint()
|
protected void |
OPBReader2005.endConstraint()
|
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)
|
IProblem |
OPBReader2010.parseInstance(Reader input)
|
IProblem |
OPBReader2005.parseInstance(Reader input)
|
IProblem |
PBInstanceReader.parseInstance(String filename)
|
protected void |
OPBReader2005.readConstraint()
read a constraint calls beginConstraint, constraintTerm and endConstraint |
| Uses of ContradictionException in org.sat4j.pb.tools |
|---|
| Methods in org.sat4j.pb.tools that throw ContradictionException | |
|---|---|
IConstr |
XplainPB.addAtLeast(IVecInt literals,
int 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 |
ClausalConstraintsDecorator.addAtLeast(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger 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 |
ClausalConstraintsDecorator.addAtLeast(IVecInt literals,
IVecInt coeffs,
int degree)
|
IConstr |
XplainPB.addAtMost(IVecInt literals,
int 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 |
ClausalConstraintsDecorator.addAtMost(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger 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 |
ClausalConstraintsDecorator.addAtMost(IVecInt literals,
IVecInt coeffs,
int degree)
|
IConstr |
XplainPB.addExactly(IVecInt literals,
int n)
|
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 |
ClausalConstraintsDecorator.addExactly(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger 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 |
ClausalConstraintsDecorator.addExactly(IVecInt literals,
IVecInt coeffs,
int weight)
|
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)
|
IConstr |
ClausalConstraintsDecorator.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> |
ImplicationRHS.implies(T... things)
Build an implication with a disjunction of literals in the RHS. |
ImplicationNamer<T,C> |
DisjunctionRHS.implies(T... things)
|
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. |
| Uses of ContradictionException in org.sat4j.reader |
|---|
| Methods in org.sat4j.reader that throw ContradictionException | |
|---|---|
protected void |
GroupedCNFReader.flushConstraint()
|
protected void |
DimacsReader.flushConstraint()
|
protected boolean |
GroupedCNFReader.handleLine()
|
protected boolean |
DimacsReader.handleLine()
|
IProblem |
XMLCSPReader.parseInstance(InputStream in)
|
IProblem |
CSPReader.parseInstance(InputStream in)
|
abstract IProblem |
Reader.parseInstance(InputStream in)
Read a file from a stream. |
IProblem |
LecteurDimacs.parseInstance(InputStream input)
|
IProblem |
InstanceReader.parseInstance(InputStream in)
|
IProblem |
DimacsReader.parseInstance(InputStream in)
|
IProblem |
AIGReader.parseInstance(InputStream in)
|
IProblem |
AAGReader.parseInstance(InputStream in)
|
IProblem |
XMLCSPReader.parseInstance(Reader in)
|
IProblem |
CSPReader.parseInstance(Reader in)
|
IProblem |
CSPInstanceReader.parseInstance(Reader in)
|
IProblem |
Reader.parseInstance(Reader in)
Deprecated. |
IProblem |
XMLCSPReader.parseInstance(String filename)
|
IProblem |
CSPInstanceReader.parseInstance(String filename)
|
IProblem |
Reader.parseInstance(String filename)
This is the usual method to feed a solver with a benchmark. |
IProblem |
InstanceReader.parseInstance(String filename)
|
protected void |
DimacsReader.readConstrs()
|
| Uses of ContradictionException in org.sat4j.sat |
|---|
| Methods in org.sat4j.sat that throw ContradictionException | |
|---|---|
protected IProblem |
Lanceur.readProblem(String problemname)
|
| Uses of ContradictionException in org.sat4j.specs |
|---|
| Methods in org.sat4j.specs that throw ContradictionException | |
|---|---|
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 |
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. |
| Uses of ContradictionException in org.sat4j.tools |
|---|
| Methods in org.sat4j.tools that throw ContradictionException | |
|---|---|
void |
SolverDecorator.addAllClauses(IVec<IVecInt> clauses)
|
void |
ManyCore.addAllClauses(IVec<IVecInt> clauses)
|
void |
AbstractOutputSolver.addAllClauses(IVec<IVecInt> clauses)
|
IConstr |
SolverDecorator.addAtLeast(IVecInt literals,
int degree)
|
IConstr |
ManyCore.addAtLeast(IVecInt literals,
int degree)
|
IConstr |
DimacsStringSolver.addAtLeast(IVecInt literals,
int degree)
|
IConstr |
DimacsOutputSolver.addAtLeast(IVecInt literals,
int degree)
|
IConstr |
ClausalCardinalitiesDecorator.addAtLeast(IVecInt literals,
int k)
|
IConstr |
SolverDecorator.addAtMost(IVecInt literals,
int degree)
|
IConstr |
ManyCore.addAtMost(IVecInt literals,
int degree)
|
IConstr |
DimacsStringSolver.addAtMost(IVecInt literals,
int degree)
|
IConstr |
DimacsOutputSolver.addAtMost(IVecInt literals,
int degree)
|
IConstr |
ClausalCardinalitiesDecorator.addAtMost(IVecInt literals,
int k)
|
IConstr |
SolverDecorator.addBlockingClause(IVecInt literals)
|
IConstr |
ManyCore.addBlockingClause(IVecInt literals)
|
IConstr |
AbstractOutputSolver.addBlockingClause(IVecInt literals)
|
IConstr |
SolverDecorator.addClause(IVecInt literals)
|
IConstr |
ManyCore.addClause(IVecInt literals)
|
IConstr |
DimacsStringSolver.addClause(IVecInt literals)
|
IConstr |
DimacsOutputSolver.addClause(IVecInt literals)
|
IConstr |
SolverDecorator.addExactly(IVecInt literals,
int n)
|
IConstr |
ManyCore.addExactly(IVecInt literals,
int n)
|
IConstr |
DimacsStringSolver.addExactly(IVecInt literals,
int n)
|
IConstr |
DimacsOutputSolver.addExactly(IVecInt literals,
int n)
|
IConstr |
ClausalCardinalitiesDecorator.addExactly(IVecInt literals,
int k)
|
void |
GateTranslator.additionalFullAdderConstraints(int xcarry,
int xsum,
int a,
int b,
int c)
|
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 |
ExtendedDimacsArrayReader.handleConstr(int gateType,
int output,
int[] inputs)
Handles a single constraint (constraint == Extended Dimacs circuit gate). |
protected boolean |
DimacsArrayReader.handleConstr(int gateType,
int output,
int[] inputs)
|
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. |
| Uses of ContradictionException in org.sat4j.tools.encoding |
|---|
| Methods in org.sat4j.tools.encoding that throw ContradictionException | |
|---|---|
IConstr |
Product.addAtLeast(ISolver solver,
IVecInt literals,
int k)
|
IConstr |
Policy.addAtLeast(ISolver solver,
IVecInt literals,
int n)
|
IConstr |
EncodingStrategyAdapter.addAtLeast(ISolver solver,
IVecInt literals,
int degree)
|
IConstr |
Commander.addAtLeast(ISolver solver,
IVecInt literals,
int k)
|
IConstr |
Binomial.addAtLeast(ISolver solver,
IVecInt literals,
int degree)
|
IConstr |
Binary.addAtLeast(ISolver solver,
IVecInt literals,
int k)
|
IConstr |
EncodingStrategyAdapter.addAtLeastOne(ISolver solver,
IVecInt literals)
|
IConstr |
Binomial.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 |
Product.addAtMost(ISolver solver,
IVecInt literals,
int k)
|
IConstr |
Policy.addAtMost(ISolver solver,
IVecInt literals,
int k)
|
IConstr |
EncodingStrategyAdapter.addAtMost(ISolver solver,
IVecInt literals,
int degree)
|
IConstr |
Commander.addAtMost(ISolver solver,
IVecInt literals,
int degree)
|
IConstr |
Binomial.addAtMost(ISolver solver,
IVecInt literals,
int degree)
|
IConstr |
Binary.addAtMost(ISolver solver,
IVecInt literals,
int k)
|
IConstr |
Product.addAtMostNonOpt(ISolver solver,
IVecInt literals,
int k)
|
IConstr |
Product.addAtMostOne(ISolver solver,
IVecInt literals)
|
IConstr |
Ladder.addAtMostOne(ISolver solver,
IVecInt literals)
|
IConstr |
EncodingStrategyAdapter.addAtMostOne(ISolver solver,
IVecInt literals)
|
IConstr |
Commander.addAtMostOne(ISolver solver,
IVecInt literals)
In this encoding, variables are partitioned in groups. |
IConstr |
Binomial.addAtMostOne(ISolver solver,
IVecInt literals)
|
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 |
Product.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 |
Commander.addExactly(ISolver solver,
IVecInt literals,
int degree)
|
IConstr |
Binomial.addExactly(ISolver solver,
IVecInt literals,
int degree)
|
IConstr |
Binary.addExactly(ISolver solver,
IVecInt literals,
int degree)
|
IConstr |
Product.addExactlyOne(ISolver solver,
IVecInt literals)
|
IConstr |
Ladder.addExactlyOne(ISolver solver,
IVecInt literals)
|
IConstr |
EncodingStrategyAdapter.addExactlyOne(ISolver solver,
IVecInt literals)
|
IConstr |
Commander.addExactlyOne(ISolver solver,
IVecInt literals)
|
IConstr |
Binomial.addExactlyOne(ISolver solver,
IVecInt literals)
|
IConstr |
Binary.addExactlyOne(ISolver solver,
IVecInt literals)
|
| Uses of ContradictionException in org.sat4j.tools.xplain |
|---|
| Methods in org.sat4j.tools.xplain that throw ContradictionException | |
|---|---|
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.addClause(IVecInt literals)
|
IConstr |
HighLevelXplain.addClause(IVecInt literals,
int desc)
|
IConstr |
Xplain.addExactly(IVecInt literals,
int n)
|
|
||||||||||
| PREV NEXT | FRAMES NO FRAMES | |||||||||