|
||||||||||
| PREV NEXT | FRAMES NO FRAMES | |||||||||
| Packages that use IConstr | |
|---|---|
| org.sat4j.core | Implementation of the data structures available in org.sat4j.specs. |
| org.sat4j.maxsat | MAXSAT and Weighted Max SAT framework. |
| 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.pb | Implementations of pseudo boolean constraints. |
| org.sat4j.pb.core | Implementations of pseudo boolean solvers |
| org.sat4j.pb.tools | Implementation of different tools for pseudo boolean solvers |
| 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 IConstr in org.sat4j.core |
|---|
| Classes in org.sat4j.core that implement IConstr | |
|---|---|
class |
ConstrGroup
A utility class used to manage easily group of clauses to be deleted at some point in the solver. |
| Methods in org.sat4j.core that return IConstr | |
|---|---|
IConstr |
ConstrGroup.getConstr(int i)
|
| Methods in org.sat4j.core with parameters of type IConstr | |
|---|---|
void |
ConstrGroup.add(IConstr constr)
|
| Uses of IConstr in org.sat4j.maxsat |
|---|
| Classes in org.sat4j.maxsat that implement IConstr | |
|---|---|
class |
UnitWeightedClause
|
| Methods in org.sat4j.maxsat that return IConstr | |
|---|---|
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. |
| Uses of IConstr in org.sat4j.minisat.constraints.card |
|---|
| Classes in org.sat4j.minisat.constraints.card that implement IConstr | |
|---|---|
class |
AtLeast
|
class |
MaxWatchCard
|
class |
MinWatchCard
|
| Uses of IConstr in org.sat4j.minisat.constraints.cnf |
|---|
| Classes in org.sat4j.minisat.constraints.cnf that implement IConstr | |
|---|---|
class |
BinaryClause
Data structure for binary clause. |
class |
HTClause
Lazy data structure for clause using the Head Tail data structure from SATO, The original scheme is improved by avoiding moving pointers to literals but moving the literals themselves. |
class |
LearntBinaryClause
|
class |
LearntHTClause
|
class |
LearntWLClause
|
class |
OriginalBinaryClause
|
class |
OriginalHTClause
|
class |
OriginalWLClause
|
class |
UnitClause
|
class |
UnitClauses
|
class |
WLClause
Lazy data structure for clause using Watched Literals. |
| Uses of IConstr in org.sat4j.minisat.core |
|---|
| Subinterfaces of IConstr in org.sat4j.minisat.core | |
|---|---|
interface |
Constr
Basic constraint abstraction used in Solver. |
| Methods in org.sat4j.minisat.core that return IConstr | |
|---|---|
IConstr |
Solver.addAtLeast(IVecInt literals,
int degree)
|
IConstr |
Solver.addAtMost(IVecInt literals,
int degree)
|
IConstr |
Solver.addBlockingClause(IVecInt literals)
|
IConstr |
Solver.addClause(IVecInt literals)
|
protected IConstr |
Solver.addConstr(Constr constr)
|
IConstr |
Solver.addExactly(IVecInt literals,
int n)
|
IConstr |
Solver.getIthConstr(int i)
returns the ith constraint in the solver. |
| Methods in org.sat4j.minisat.core with parameters of type IConstr | |
|---|---|
boolean |
Solver.removeConstr(IConstr co)
|
boolean |
Solver.removeSubsumedConstr(IConstr co)
|
| Uses of IConstr in org.sat4j.opt |
|---|
| Methods in org.sat4j.opt that return IConstr | |
|---|---|
IConstr |
MaxSatDecorator.addClause(IVecInt literals)
|
| Uses of IConstr in org.sat4j.pb |
|---|
| Methods in org.sat4j.pb that return IConstr | |
|---|---|
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" |
| Uses of IConstr in org.sat4j.pb.constraints.pb |
|---|
| Subinterfaces of IConstr in org.sat4j.pb.constraints.pb | |
|---|---|
interface |
IWatchPb
|
interface |
PBConstr
|
| Classes in org.sat4j.pb.constraints.pb that implement IConstr | |
|---|---|
class |
AtLeastPB
|
class |
LearntBinaryClausePB
|
class |
LearntHTClausePB
|
class |
MaxWatchPb
Data structure for pseudo-boolean constraint with watched literals. |
class |
MaxWatchPbLong
Data structure for pseudo-boolean constraint with watched literals. |
class |
MaxWatchPbLongCP
Data structure for pseudo-boolean constraint with watched literals. |
class |
MinWatchCardPB
|
class |
MinWatchPb
Data structure for pseudo-boolean constraint with watched literals. |
class |
MinWatchPbLong
Data structure for pseudo-boolean constraint with watched literals. |
class |
MinWatchPbLongCP
Data structure for pseudo-boolean constraint with watched literals. |
class |
MinWatchPbLongLimit
Data structure for pseudo-boolean constraint with watched literals. |
class |
OriginalBinaryClausePB
|
class |
OriginalHTClausePB
|
class |
PuebloMinWatchPb
|
class |
UnitClausePB
|
class |
UnitClausesPB
|
class |
WatchPb
Abstract data structure for pseudo-boolean constraint with watched literals. |
class |
WatchPbLong
|
class |
WatchPbLongCP
|
| Uses of IConstr in org.sat4j.pb.core |
|---|
| Methods in org.sat4j.pb.core that return IConstr | |
|---|---|
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)
|
| Uses of IConstr in org.sat4j.pb.tools |
|---|
| Methods in org.sat4j.pb.tools that return IConstr | |
|---|---|
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)
|
protected IConstr |
LexicoDecoratorPB.discardSolutionsForOptimizing()
|
| Methods in org.sat4j.pb.tools with parameters of type IConstr | |
|---|---|
void |
ConflictTracing.learn(IConstr c)
|
| Constructor parameters in org.sat4j.pb.tools with type arguments of type IConstr | |
|---|---|
ImplicationNamer(DependencyHelper<T,C> helper,
IVec<IConstr> toName)
|
|
| Uses of IConstr in org.sat4j.sat |
|---|
| Methods in org.sat4j.sat with parameters of type IConstr | |
|---|---|
void |
DetailedCommandPanel.conflictFound(IConstr confl,
int dlevel,
int trailLevel)
|
void |
DetailedCommandPanel.learn(IConstr c)
|
void |
DetailedCommandPanel.propagating(int p,
IConstr reason)
|
| Uses of IConstr in org.sat4j.specs |
|---|
| Methods in org.sat4j.specs that return IConstr | |
|---|---|
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". |
| Methods in org.sat4j.specs that return types with arguments of type IConstr | |
|---|---|
IVec<? extends IConstr> |
ISolverService.getLearnedConstraints()
Read-Only access to the list of constraints learned and not deleted so far in the solver. |
| Methods in org.sat4j.specs with parameters of type IConstr | |
|---|---|
void |
SearchListener.conflictFound(IConstr confl,
int dlevel,
int trailLevel)
a conflict has been found. |
void |
SearchListener.learn(IConstr c)
learning a new clause |
void |
SearchListener.propagating(int p,
IConstr reason)
Unit propagation |
boolean |
ISolver.removeConstr(IConstr c)
Remove a constraint returned by one of the add method from the solver. |
boolean |
ISolver.removeSubsumedConstr(IConstr c)
Remove a constraint returned by one of the add method from the solver that is subsumed by a constraint already in the solver or to be added to the solver. |
| Uses of IConstr in org.sat4j.tools |
|---|
| Methods in org.sat4j.tools that return IConstr | |
|---|---|
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)
|
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. |
protected IConstr |
LexicoDecorator.discardSolutionsForOptimizing()
|
IConstr |
GateTranslator.gateFalse(int y)
translate y <=> FALSE into a clause. |
IConstr |
GateTranslator.gateTrue(int y)
translate y <=> TRUE into a clause. |
IConstr[] |
GateTranslator.halfOr(int y,
IVecInt literals)
translate y <= x1 \/ x2 \/ ... \/ xn into clauses. |
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. |
IConstr[] |
GateTranslator.or(int y,
IVecInt literals)
translate y <=> x1 \/ x2 \/ ... \/ xn into clauses. |
IConstr[] |
GateTranslator.xor(int y,
IVecInt literals)
translate y <=> x1 xor x2 xor ... xor xn into clauses. |
| Methods in org.sat4j.tools with parameters of type IConstr | |
|---|---|
void |
TextOutputTracing.conflictFound(IConstr confl,
int dlevel,
int trailLevel)
|
void |
SearchListenerAdapter.conflictFound(IConstr confl,
int dlevel,
int trailLevel)
|
void |
MultiTracing.conflictFound(IConstr confl,
int dlevel,
int trailLevel)
|
void |
LearnedClauseSizeTracing.conflictFound(IConstr confl,
int dlevel,
int trailLevel)
|
void |
LBDTracing.conflictFound(IConstr confl,
int dlevel,
int trailLevel)
|
void |
DotSearchTracing.conflictFound(IConstr confl,
int dlevel,
int trailLevel)
|
void |
DecisionLevelTracing.conflictFound(IConstr confl,
int dlevel,
int trailLevel)
|
void |
ConflictLevelTracing.conflictFound(IConstr confl,
int dlevel,
int trailLevel)
|
void |
ConflictDepthTracing.conflictFound(IConstr confl,
int dlevel,
int trailLevel)
|
void |
TextOutputTracing.learn(IConstr clause)
|
void |
SearchListenerAdapter.learn(IConstr c)
|
void |
MultiTracing.learn(IConstr c)
|
void |
LearnedClausesSizeTracing.learn(IConstr c)
|
void |
DotSearchTracing.learn(IConstr clause)
|
void |
TextOutputTracing.propagating(int p,
IConstr reason)
|
void |
SpeedTracing.propagating(int p,
IConstr reason)
|
void |
SearchListenerAdapter.propagating(int p,
IConstr reason)
|
void |
MultiTracing.propagating(int p,
IConstr reason)
|
void |
DotSearchTracing.propagating(int p,
IConstr reason)
|
boolean |
SolverDecorator.removeConstr(IConstr c)
|
boolean |
ManyCore.removeConstr(IConstr c)
|
boolean |
AbstractOutputSolver.removeConstr(IConstr c)
|
boolean |
SolverDecorator.removeSubsumedConstr(IConstr c)
|
boolean |
ManyCore.removeSubsumedConstr(IConstr c)
|
boolean |
AbstractOutputSolver.removeSubsumedConstr(IConstr c)
|
| Uses of IConstr in org.sat4j.tools.encoding |
|---|
| Methods in org.sat4j.tools.encoding that return IConstr | |
|---|---|
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 IConstr in org.sat4j.tools.xplain |
|---|
| Fields in org.sat4j.tools.xplain with type parameters of type IConstr | |
|---|---|
protected Map<Integer,IConstr> |
Xplain.constrs
|
| Methods in org.sat4j.tools.xplain that return IConstr | |
|---|---|
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)
|
| Methods in org.sat4j.tools.xplain that return types with arguments of type IConstr | |
|---|---|
Collection<IConstr> |
Xplain.explain()
|
Collection<IConstr> |
Xplain.getConstraints()
|
| Methods in org.sat4j.tools.xplain with parameters of type IConstr | |
|---|---|
boolean |
Xplain.removeConstr(IConstr c)
|
boolean |
Xplain.removeSubsumedConstr(IConstr c)
|
|
||||||||||
| PREV NEXT | FRAMES NO FRAMES | |||||||||