|
||||||||||
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.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)
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 | |
---|---|
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 MinWatchPb |
MinWatchPb.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,
IVecInt coefs,
boolean moreThan,
int degree)
|
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.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 |
void |
OPBReader2005.parseInstance(java.io.LineNumberReader in)
|
void |
GoodOPBReader.parseInstance(java.io.LineNumberReader in)
|
void |
DimacsReader.parseInstance(java.io.LineNumberReader in)
|
void |
CSPReader.parseInstance(java.io.LineNumberReader in)
|
IProblem |
OPBReader2005.parseInstance(java.lang.String filename)
|
IProblem |
LecteurDimacs.parseInstance(java.lang.String nomFichier)
lit la base de clauses et la met dans le vecteur donn? |
IProblem |
InstanceReader.parseInstance(java.lang.String filename)
|
IProblem |
GoodOPBReader.parseInstance(java.lang.String filename)
|
IProblem |
DimacsReader.parseInstance(java.lang.String filename)
Remplit un prouveur ? |
IProblem |
CSPReader.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" |
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 |