|
||||||||||
| PREV NEXT | FRAMES NO FRAMES | |||||||||
| Packages that use ContradictionException | |
|---|---|
| org.sat4j.minisat.constraints | Implementations of various constraints for MiniSAT. |
| org.sat4j.minisat.constraints.card | Implementations of cardinality contraints. |
| org.sat4j.minisat.constraints.cnf | Implementations of clausal contraints. |
| org.sat4j.minisat.constraints.pb | Implementations of pseudo boolean contraints. |
| org.sat4j.minisat.core | Implementation of the MiniSAT solver skeleton. |
| org.sat4j.opt | Optimization extensions. |
| org.sat4j.reader | Some utility classes to read problems from plain text files. |
| org.sat4j.specs | Those classes are intented for users dealing with SAT solvers as blackboxes. |
| org.sat4j.tools | Tools to be used on top of an ISolver. |
| Uses of ContradictionException in org.sat4j.minisat.constraints |
|---|
| Methods in org.sat4j.minisat.constraints that throw ContradictionException | |
|---|---|
Constr |
MixedDataStructureDaniel.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 |
AbstractPBDataStructureFactory.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
AbstractDataStructureFactory.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
MixedDataStructureWithBinaryAndTernary.createClause(IVecInt literals)
|
Constr |
MixedDataStructureWithBinary.createClause(IVecInt literals)
|
Constr |
ClausalDataStructureWL.createClause(IVecInt literals)
|
Constr |
ClausalDataStructureCBWL.createClause(IVecInt literals)
|
Constr |
ClausalDataStructureCB.createClause(IVecInt literals)
|
Constr |
CardinalityDataStructureYanMin.createClause(IVecInt literals)
|
Constr |
CardinalityDataStructureYanMax.createClause(IVecInt literals)
|
Constr |
CardinalityDataStructure.createClause(IVecInt literals)
|
Constr |
AbstractPBDataStructureFactory.createClause(IVecInt literals)
|
Constr |
AbstractPBDataStructureFactory.createPseudoBooleanConstraint(IVecInt literals,
IVec<java.math.BigInteger> coefs,
boolean moreThan,
java.math.BigInteger degree)
|
Constr |
AbstractDataStructureFactory.createPseudoBooleanConstraint(IVecInt literals,
IVec<java.math.BigInteger> coefs,
boolean moreThan,
java.math.BigInteger degree)
|
Constr |
AbstractCardinalityDataStructure.createPseudoBooleanConstraint(IVecInt literals,
IVec<java.math.BigInteger> coefs,
boolean moreThan,
java.math.BigInteger degree)
|
IConstr |
AbstractPBDataStructureFactory.createUnregisteredPseudoBooleanConstraint(IVecInt literals,
IVec<java.math.BigInteger> coefs,
boolean moreThan,
java.math.BigInteger degree)
|
| Uses of ContradictionException in org.sat4j.minisat.constraints.card |
|---|
| Methods in org.sat4j.minisat.constraints.card that throw ContradictionException | |
|---|---|
static AtLeast |
AtLeast.atLeastNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
int n)
|
static MaxWatchCard |
MaxWatchCard.maxWatchCardNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
boolean moreThan,
int degree)
Permet la cr? |
static MinWatchCard |
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? |
| Uses of ContradictionException in org.sat4j.minisat.constraints.cnf |
|---|
| Methods in org.sat4j.minisat.constraints.cnf that throw ContradictionException | |
|---|---|
static IVecInt |
WLClause.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.constraints.pb |
|---|
| Methods in org.sat4j.minisat.constraints.pb that throw ContradictionException | |
|---|---|
IConstr |
PBSolverWithImpliedClause.addPseudoBoolean(IVecInt literals,
IVec<java.math.BigInteger> coeffs,
boolean moreThan,
java.math.BigInteger degree)
|
static AtLeastPB |
AtLeastPB.atLeastNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
int n)
|
static MaxWatchPb |
MaxWatchPb.maxWatchPbNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
IVec<java.math.BigInteger> coefs,
boolean moreThan,
java.math.BigInteger degree)
|
static MaxWatchPb |
MaxWatchPb.maxWatchPbNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
IVecInt coefs,
boolean moreThan,
int degree)
|
static MinWatchCardPB |
MinWatchCardPB.minWatchCardPBNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
boolean moreThan,
int degree)
Permet la cr? |
static PuebloMinWatchPb |
PuebloMinWatchPb.minWatchPbNew(UnitPropagationListener s,
ILits voc,
IDataStructurePB mpb)
|
static PuebloMinWatchPb |
PuebloMinWatchPb.minWatchPbNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
IVec<java.math.BigInteger> coefs,
boolean moreThan,
java.math.BigInteger degree)
|
static MinWatchPb |
MinWatchPb.minWatchPbNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
IVec<java.math.BigInteger> coefs,
boolean moreThan,
java.math.BigInteger degree)
|
static PuebloMinWatchPb |
PuebloMinWatchPb.minWatchPbNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
IVecInt coefs,
boolean moreThan,
int degree)
|
static MinWatchPb |
MinWatchPb.minWatchPbNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
IVecInt coefs,
boolean moreThan,
int degree)
|
static IDataStructurePB |
WatchPb.niceParameters(IVecInt ps,
IVec<java.math.BigInteger> bigCoefs,
boolean moreThan,
java.math.BigInteger bigDeg,
ILits voc)
|
static MaxWatchPb |
MaxWatchPb.normalizedMaxWatchPbNew(UnitPropagationListener s,
ILits voc,
ArrayPb mpb)
|
static MaxWatchPb |
MaxWatchPb.normalizedMaxWatchPbNew(UnitPropagationListener s,
ILits voc,
IDataStructurePB mpb)
|
static MinWatchCardPB |
MinWatchCardPB.normalizedMinWatchCardPBNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
int degree)
Permet la cr? |
static MinWatchPb |
MinWatchPb.normalizedMinWatchPbNew(UnitPropagationListener s,
ILits voc,
IDataStructurePB mpb)
|
static WatchPb |
MinWatchPb.normalizedWatchPbNew(ILits voc,
IDataStructurePB mpb)
|
| 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.addClause(IVecInt literals)
|
IConstr |
Solver.addPseudoBoolean(IVecInt literals,
IVec<java.math.BigInteger> coeffs,
boolean moreThan,
java.math.BigInteger degree)
|
Constr |
DataStructureFactory.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
DataStructureFactory.createClause(IVecInt literals)
|
Constr |
DataStructureFactory.createPseudoBooleanConstraint(IVecInt literals,
IVec<java.math.BigInteger> coefs,
boolean moreThan,
java.math.BigInteger degree)
|
| Uses of ContradictionException in org.sat4j.opt |
|---|
| Methods in org.sat4j.opt that throw ContradictionException | |
|---|---|
IConstr |
WeightedMaxSatDecorator.addClause(IVecInt literals)
|
IConstr |
MaxSatDecorator.addClause(IVecInt literals)
|
void |
WeightedMaxSatDecorator.discard()
|
void |
PseudoOptDecorator.discard()
|
void |
MinOneDecorator.discard()
|
void |
MaxSatDecorator.discard()
|
| Uses of ContradictionException in org.sat4j.reader |
|---|
| Methods in org.sat4j.reader that throw ContradictionException | |
|---|---|
void |
OPBReader2005.parse()
parses the file and uses the callbacks to send to send the data back to the program |
IProblem |
LecteurDimacs.parseInstance(java.io.InputStream in)
|
IProblem |
Reader.parseInstance(java.io.InputStream in)
|
IProblem |
OPBReader2005.parseInstance(java.io.Reader in)
|
IProblem |
LecteurDimacs.parseInstance(java.io.Reader in)
|
IProblem |
InstanceReader.parseInstance(java.io.Reader in)
|
IProblem |
GoodOPBReader.parseInstance(java.io.Reader in)
|
IProblem |
DimacsReader.parseInstance(java.io.Reader in)
|
IProblem |
CSPReader.parseInstance(java.io.Reader in)
|
abstract IProblem |
Reader.parseInstance(java.io.Reader in)
|
IProblem |
InstanceReader.parseInstance(java.lang.String filename)
|
IProblem |
Reader.parseInstance(java.lang.String filename)
|
| 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.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.addPseudoBoolean(IVecInt lits,
IVec<java.math.BigInteger> coeffs,
boolean moreThan,
java.math.BigInteger d)
Create a Pseudo-Boolean constraint of the type "at least n of those literals must be satisfied" |
void |
IOptimizationProblem.discard()
|
| Uses of ContradictionException in org.sat4j.tools |
|---|
| Methods in org.sat4j.tools that throw ContradictionException | |
|---|---|
void |
SolverDecorator.addAllClauses(IVec<IVecInt> clauses)
|
IConstr |
SolverDecorator.addAtLeast(IVecInt literals,
int degree)
|
IConstr |
SolverDecorator.addAtMost(IVecInt literals,
int degree)
|
IConstr |
SolverDecorator.addClause(IVecInt literals)
|
IConstr |
SolverDecorator.addPseudoBoolean(IVecInt literals,
IVec<java.math.BigInteger> coeffs,
boolean moreThan,
java.math.BigInteger degree)
|
|
||||||||||
| PREV NEXT | FRAMES NO FRAMES | |||||||||