Uses of Interface
org.sat4j.minisat.core.Constr

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	CardinalityDataStructure.createCardinalityConstraint(IVecInt literals, int degree)
Constr	CardinalityDataStructureYanMax.createCardinalityConstraint(IVecInt literals, int degree)
Constr	CardinalityDataStructureYanMin.createCardinalityConstraint(IVecInt literals, int degree)
Constr	MixedDataStructureDaniel.createCardinalityConstraint(IVecInt literals, int degree)
Constr	CardinalityDataStructure.createClause(IVecInt literals)
Constr	CardinalityDataStructureYanMax.createClause(IVecInt literals)
Constr	CardinalityDataStructureYanMin.createClause(IVecInt literals)
Constr	ClausalDataStructureCB.createClause(IVecInt literals)
Constr	ClausalDataStructureCBWL.createClause(IVecInt literals)
Constr	ClausalDataStructureWL.createClause(IVecInt literals)
Constr	MixedDataStructureDaniel.createClause(IVecInt literals)
Constr	MixedDataStructureDanielCBWL.createClause(IVecInt literals)
Constr	MixedDataStructureWithBinary.createClause(IVecInt literals)
Constr	MixedDataStructureWithBinaryAndTernary.createClause(IVecInt literals)
Constr	CardinalityDataStructure.createUnregisteredClause(IVecInt literals)
Constr	CardinalityDataStructureYanMax.createUnregisteredClause(IVecInt literals)
Constr	CardinalityDataStructureYanMin.createUnregisteredClause(IVecInt literals)
Constr	ClausalDataStructureCB.createUnregisteredClause(IVecInt literals)
Constr	ClausalDataStructureCBWL.createUnregisteredClause(IVecInt literals)
Constr	ClausalDataStructureWL.createUnregisteredClause(IVecInt literals)
Constr	MixedDataStructureDaniel.createUnregisteredClause(IVecInt literals)
Constr	MixedDataStructureWithBinary.createUnregisteredClause(IVecInt literals)
Constr	MixedDataStructureWithBinaryAndTernary.createUnregisteredClause(IVecInt literals)

Methods in org.sat4j.minisat.constraints with parameters of type Constr

void	AbstractDataStructureFactory.learnConstraint(Constr constr)
void	MixedDataStructureWithBinary.learnConstraint(Constr constr)
void	MixedDataStructureWithBinaryAndTernary.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

Uses of Constr in org.sat4j.minisat.constraints.cnf

Classes in org.sat4j.minisat.constraints.cnf that implement Constr

class	BinaryClauses
class	CBClause
class	DefaultWLClause
class	LearntWLClause
class	MixableCBClause Counter Based clauses that can be mixed with WLCLauses
class	OriginalWLClause
class	TernaryClauses
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

void	Solver.analyze(Constr confl, Pair results)
void	Solver.claBumpActivity(Constr confl) Propagate activity to a constraint
boolean	Solver.enqueue(int p, Constr from) Put the literal on the queue of assignments to be done.
boolean	UnitPropagationListener.enqueue(int p, Constr from) satisfies a literal
void	DotSearchListener.learn(Constr clause)
void	Learner.learn(Constr c)
void	SearchListener.learn(Constr c) learning a new clause
void	Solver.learn(Constr c)
void	TextOutputListener.learn(Constr clause)
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

void	LimitedLearning.learns(Constr constr)
void	MiniSATLearning.learns(Constr constr)
void	NoLearningButHeuristics.learns(Constr reason)
void	NoLearningNoHeuristics.learns(Constr reason)