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.constraints.pb	Implementations of pseudo boolean 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	AbstractPBDataStructureFactory.createCardinalityConstraint(IVecInt literals, int degree)
Constr	CardinalityDataStructureYanMax.createCardinalityConstraint(IVecInt literals, int degree)
Constr	CardinalityDataStructure.createCardinalityConstraint(IVecInt literals, int degree)
Constr	CardinalityDataStructureYanMin.createCardinalityConstraint(IVecInt literals, int degree)
Constr	MixedDataStructureDaniel.createCardinalityConstraint(IVecInt literals, int degree)
Constr	AbstractDataStructureFactory.createCardinalityConstraint(IVecInt literals, int degree)
Constr	MixedDataStructureDanielCBWL.createClause(IVecInt literals)
Constr	AbstractPBDataStructureFactory.createClause(IVecInt literals)
Constr	CardinalityDataStructureYanMax.createClause(IVecInt literals)
Constr	CardinalityDataStructure.createClause(IVecInt literals)
Constr	CardinalityDataStructureYanMin.createClause(IVecInt literals)
Constr	ClausalDataStructureWL.createClause(IVecInt literals)
Constr	ClausalDataStructureCBWL.createClause(IVecInt literals)
Constr	ClausalDataStructureCB.createClause(IVecInt literals)
Constr	MixedDataStructureWithBinaryAndTernary.createClause(IVecInt literals)
Constr	MixedDataStructureDaniel.createClause(IVecInt literals)
Constr	MixedDataStructureWithBinary.createClause(IVecInt literals)
Constr	AbstractPBDataStructureFactory.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)
Constr	AbstractDataStructureFactory.createPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
Constr	AbstractPBDataStructureFactory.createUnregisteredClause(IVecInt literals)
Constr	CardinalityDataStructureYanMax.createUnregisteredClause(IVecInt literals)
Constr	CardinalityDataStructure.createUnregisteredClause(IVecInt literals)
Constr	CardinalityDataStructureYanMin.createUnregisteredClause(IVecInt literals)
Constr	ClausalDataStructureWL.createUnregisteredClause(IVecInt literals)
Constr	ClausalDataStructureCBWL.createUnregisteredClause(IVecInt literals)
Constr	ClausalDataStructureCB.createUnregisteredClause(IVecInt literals)
Constr	MixedDataStructureWithBinaryAndTernary.createUnregisteredClause(IVecInt literals)
Constr	MixedDataStructureDaniel.createUnregisteredClause(IVecInt literals)
Constr	MixedDataStructureWithBinary.createUnregisteredClause(IVecInt literals)
Constr	AbstractPBDataStructureFactory.createUnregisteredPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)
Constr	AbstractDataStructureFactory.createUnregisteredPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)

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

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

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.constraints.pb

Subinterfaces of Constr in org.sat4j.minisat.constraints.pb

interface

PBConstr

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

class	AtLeastPB
class	MaxWatchPb
class	MinWatchCardPB
class	MinWatchPb
class	MixableCBClausePB
class	PuebloMinWatchPb
class	WatchPb
class	WLClausePB

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

int	PBSolver.analyze(Constr myconfl, Handle<Constr> outLearntRef)

Method parameters in org.sat4j.minisat.constraints.pb with type arguments of type Constr

int	PBSolver.analyze(Constr myconfl, Handle<Constr> outLearntRef)

Uses of Constr in org.sat4j.minisat.core

Methods in org.sat4j.minisat.core that return Constr

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)
Constr	DataStructureFactory.createUnregisteredClause(IVecInt literals)
Constr	DataStructureFactory.createUnregisteredPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)
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)
int	Solver.analyze(Constr confl, Handle<Constr> outLearntRef)
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	Solver.learn(Constr c)
void	TextOutputListener.learn(Constr clause)
void	DotSearchListener.learn(Constr clause)
void	Learner.learn(Constr c)
void	SearchListener.learn(Constr c) learning a new clause
void	DataStructureFactory.learnConstraint(Constr constr)
void	LearningStrategy.learns(Constr constr)
void	ILits.setReason(int lit, Constr r)

Method parameters in org.sat4j.minisat.core with type arguments of type Constr

int	Solver.analyze(Constr confl, Handle<Constr> outLearntRef)

Uses of Constr in org.sat4j.minisat.learning

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

protected boolean	ClauseOnlyLearning.learningCondition(Constr constr)
protected boolean	PercentLengthLearning.learningCondition(Constr constr)
protected boolean	ActiveLearning.learningCondition(Constr clause)
protected boolean	FixedLengthLearning.learningCondition(Constr constr)
protected abstract boolean	LimitedLearning.learningCondition(Constr constr)
void	NoLearningNoHeuristics.learns(Constr reason)
void	MiniSATLearning.learns(Constr constr)
void	NoLearningButHeuristics.learns(Constr reason)
void	LimitedLearning.learns(Constr constr)