|
||||||||||
PREV NEXT | FRAMES NO FRAMES |
Packages that use Constr | |
---|---|
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.core | Implementation of the MiniSAT solver skeleton. |
org.sat4j.minisat.learning | Various learning strategies. |
Uses of Constr in org.sat4j.minisat.constraints |
---|
Methods in org.sat4j.minisat.constraints that return Constr | |
---|---|
Constr |
AbstractDataStructureFactory.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
CardinalityDataStructureYanMin.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
MixedDataStructureDanielHT.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
CardinalityDataStructure.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
MixedDataStructureDanielWL.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
CardinalityDataStructureYanMax.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
ClausalDataStructureCB.createClause(IVecInt literals)
|
Constr |
CardinalityDataStructureYanMin.createClause(IVecInt literals)
|
Constr |
ClausalDataStructureCBWL.createClause(IVecInt literals)
|
Constr |
ClausalDataStructureWL.createClause(IVecInt literals)
|
Constr |
MixedDataStructureDanielHT.createClause(IVecInt literals)
|
Constr |
CardinalityDataStructure.createClause(IVecInt literals)
|
Constr |
MixedDataStructureDanielCBWL.createClause(IVecInt literals)
|
Constr |
MixedDataStructureDanielWL.createClause(IVecInt literals)
|
Constr |
CardinalityDataStructureYanMax.createClause(IVecInt literals)
|
Constr |
ClausalDataStructureCB.createUnregisteredClause(IVecInt literals)
|
Constr |
CardinalityDataStructureYanMin.createUnregisteredClause(IVecInt literals)
|
Constr |
ClausalDataStructureCBWL.createUnregisteredClause(IVecInt literals)
|
Constr |
ClausalDataStructureWL.createUnregisteredClause(IVecInt literals)
|
Constr |
MixedDataStructureDanielHT.createUnregisteredClause(IVecInt literals)
|
Constr |
CardinalityDataStructure.createUnregisteredClause(IVecInt literals)
|
Constr |
MixedDataStructureDanielWL.createUnregisteredClause(IVecInt literals)
|
Constr |
CardinalityDataStructureYanMax.createUnregisteredClause(IVecInt literals)
|
Methods in org.sat4j.minisat.constraints with parameters of type Constr | |
---|---|
void |
AbstractDataStructureFactory.learnConstraint(Constr constr)
|
Uses of Constr in org.sat4j.minisat.constraints.card |
---|
Classes in org.sat4j.minisat.constraints.card that implement Constr | |
---|---|
class |
AtLeast
|
class |
MaxWatchCard
|
class |
MinWatchCard
|
Methods in org.sat4j.minisat.constraints.card that return Constr | |
---|---|
static Constr |
AtLeast.atLeastNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
int n)
|
Uses of Constr in org.sat4j.minisat.constraints.cnf |
---|
Classes in org.sat4j.minisat.constraints.cnf that implement Constr | |
---|---|
class |
BinaryClause
Data structure for binary clause. |
class |
CBClause
|
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 |
MixableCBClause
Counter Based clauses that can be mixed with WLCLauses |
class |
OriginalBinaryClause
|
class |
OriginalHTClause
|
class |
OriginalWLClause
|
class |
UnitClause
|
class |
UnitClauses
|
class |
WLClause
Lazy data structure for clause using Watched Literals. |
Methods in org.sat4j.minisat.constraints.cnf that return Constr | |
---|---|
Constr |
Lits.getReason(int lit)
|
Methods in org.sat4j.minisat.constraints.cnf with parameters of type Constr | |
---|---|
void |
Lits.setReason(int lit,
Constr r)
|
Uses of Constr in org.sat4j.minisat.core |
---|
Fields in org.sat4j.minisat.core declared as Constr | |
---|---|
Constr |
Pair.reason
|
Methods in org.sat4j.minisat.core that return Constr | |
---|---|
Constr |
DataStructureFactory.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
DataStructureFactory.createClause(IVecInt literals)
|
Constr |
DataStructureFactory.createUnregisteredClause(IVecInt literals)
|
Constr |
ILits.getReason(int lit)
|
Constr |
Solver.propagate()
|
Methods in org.sat4j.minisat.core with parameters of type Constr | |
---|---|
protected IConstr |
Solver.addConstr(Constr constr)
|
void |
Solver.analyze(Constr confl,
Pair results)
|
protected void |
Solver.analyzeAtRootLevel(Constr conflict)
|
void |
Solver.claBumpActivity(Constr confl)
Propagate activity to a constraint |
boolean |
UnitPropagationListener.enqueue(int p,
Constr from)
satisfies a literal |
boolean |
Solver.enqueue(int p,
Constr from)
Put the literal on the queue of assignments to be done. |
void |
Learner.learn(Constr c)
|
void |
Solver.learn(Constr c)
|
void |
DataStructureFactory.learnConstraint(Constr constr)
|
void |
LearningStrategy.learns(Constr constr)
|
void |
ILits.setReason(int lit,
Constr r)
|
Uses of Constr in org.sat4j.minisat.learning |
---|
Methods in org.sat4j.minisat.learning with parameters of type Constr | |
---|---|
protected abstract boolean |
LimitedLearning.learningCondition(Constr constr)
|
protected boolean |
ActiveLearning.learningCondition(Constr clause)
|
protected boolean |
FixedLengthLearning.learningCondition(Constr constr)
|
protected boolean |
ClauseOnlyLearning.learningCondition(Constr constr)
|
protected boolean |
PercentLengthLearning.learningCondition(Constr constr)
|
void |
LimitedLearning.learns(Constr constr)
|
void |
NoLearningButHeuristics.learns(Constr reason)
|
void |
MiniSATLearning.learns(Constr constr)
|
void |
NoLearningNoHeuristics.learns(Constr reason)
|
|
||||||||||
PREV NEXT | FRAMES NO FRAMES |