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.
org.sat4j.pb.constraints
org.sat4j.pb.constraints.pb	Implementations of pseudo boolean contraints.
org.sat4j.pb.core

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	MixedDataStructureDanielHT.createCardinalityConstraint(IVecInt literals, int degree)
Constr	MixedDataStructureDanielWL.createCardinalityConstraint(IVecInt literals, int degree)
Constr	CardinalityDataStructureYanMin.createCardinalityConstraint(IVecInt literals, int degree)
Constr	CardinalityDataStructureYanMax.createCardinalityConstraint(IVecInt literals, int degree)
Constr	ClausalDataStructureWL.createClause(IVecInt literals)
Constr	ClausalDataStructureCB.createClause(IVecInt literals)
Constr	CardinalityDataStructure.createClause(IVecInt literals)
Constr	MixedDataStructureDanielHT.createClause(IVecInt literals)
Constr	MixedDataStructureDanielWL.createClause(IVecInt literals)
Constr	MixedDataStructureDanielCBWL.createClause(IVecInt literals)
Constr	CardinalityDataStructureYanMin.createClause(IVecInt literals)
Constr	ClausalDataStructureCBWL.createClause(IVecInt literals)
Constr	CardinalityDataStructureYanMax.createClause(IVecInt literals)
Constr	ClausalDataStructureWL.createUnregisteredClause(IVecInt literals)
Constr	ClausalDataStructureCB.createUnregisteredClause(IVecInt literals)
Constr	CardinalityDataStructure.createUnregisteredClause(IVecInt literals)
Constr	MixedDataStructureDanielHT.createUnregisteredClause(IVecInt literals)
Constr	MixedDataStructureDanielWL.createUnregisteredClause(IVecInt literals)
Constr	CardinalityDataStructureYanMin.createUnregisteredClause(IVecInt literals)
Constr	ClausalDataStructureCBWL.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)
IVecInt	Solver.analyzeFinalConflictInTermsOfAssumptions(Constr confl, IVecInt assumps, int conflictingLiteral) Derive a subset of the assumptions causing the inconistency.
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	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 boolean	ClauseOnlyLearning.learningCondition(Constr constr)
protected abstract boolean	LimitedLearning.learningCondition(Constr constr)
protected boolean	PercentLengthLearning.learningCondition(Constr constr)
protected boolean	ActiveLearning.learningCondition(Constr clause)
protected boolean	FixedLengthLearning.learningCondition(Constr constr)
void	MiniSATLearning.learns(Constr constr)
void	NoLearningButHeuristics.learns(Constr reason)
void	NoLearningNoHeuristics.learns(Constr reason)
void	LimitedLearning.learns(Constr constr)

Uses of Constr in org.sat4j.pb.constraints

Methods in org.sat4j.pb.constraints that return Constr

protected abstract Constr	AbstractPBDataStructureFactory.constraintFactory(int[] literals, BigInteger[] coefs, BigInteger degree)
protected Constr	AbstractPBClauseCardConstrDataStructure.constraintFactory(int[] literals, BigInteger[] coefs, BigInteger degree)
protected Constr	PBMaxDataStructure.constraintFactory(int[] literals, BigInteger[] coefs, BigInteger degree)
protected Constr	CompetResolutionPBMixedHTClauseCardConstrDataStructure.constructCard(IVecInt theLits, int degree)
protected abstract Constr	AbstractPBClauseCardConstrDataStructure.constructCard(IVecInt theLits, int degree)
protected Constr	CompetResolutionPBMixedWLClauseCardConstrDataStructure.constructCard(IVecInt theLits, int degree)
protected Constr	CompetMinHTmixedClauseCardConstrDataStructureFactory.constructCard(IVecInt theLits, int degree)
protected Constr	PuebloPBMinClauseCardConstrDataStructure.constructCard(IVecInt theLits, int degree)
protected Constr	CompetResolutionPBMixedHTClauseCardConstrDataStructure.constructClause(IVecInt v)
protected abstract Constr	AbstractPBClauseCardConstrDataStructure.constructClause(IVecInt v)
protected Constr	CompetResolutionPBMixedWLClauseCardConstrDataStructure.constructClause(IVecInt v)
protected Constr	CompetMinHTmixedClauseCardConstrDataStructureFactory.constructClause(IVecInt v)
protected Constr	PuebloPBMinClauseCardConstrDataStructure.constructClause(IVecInt v)
protected Constr	CompetResolutionPBMixedHTClauseCardConstrDataStructure.constructLearntCard(IDataStructurePB dspb)
protected Constr	PBMaxClauseAtLeastConstrDataStructure.constructLearntCard(IDataStructurePB dspb)
protected abstract Constr	AbstractPBClauseCardConstrDataStructure.constructLearntCard(IDataStructurePB dspb)
protected Constr	CompetResolutionPBMixedWLClauseCardConstrDataStructure.constructLearntCard(IDataStructurePB dspb)
protected Constr	CompetMinHTmixedClauseCardConstrDataStructureFactory.constructLearntCard(IDataStructurePB dspb)
protected Constr	PuebloPBMinClauseAtLeastConstrDataStructure.constructLearntCard(IDataStructurePB dspb)
protected Constr	PuebloPBMinClauseCardConstrDataStructure.constructLearntCard(IDataStructurePB dspb)
protected Constr	CompetResolutionPBMixedHTClauseCardConstrDataStructure.constructLearntClause(IVecInt resLits)
protected abstract Constr	AbstractPBClauseCardConstrDataStructure.constructLearntClause(IVecInt literals)
protected Constr	CompetResolutionPBMixedWLClauseCardConstrDataStructure.constructLearntClause(IVecInt resLits)
protected Constr	CompetMinHTmixedClauseCardConstrDataStructureFactory.constructLearntClause(IVecInt resLits)
protected Constr	PuebloPBMinClauseCardConstrDataStructure.constructLearntClause(IVecInt literals)
protected abstract Constr	AbstractPBClauseCardConstrDataStructure.constructLearntPB(IDataStructurePB dspb)
protected Constr	PuebloPBMinClauseCardConstrDataStructure.constructLearntPB(IDataStructurePB dspb)
protected Constr	PBMaxClauseCardConstrDataStructure.constructLearntPB(IDataStructurePB mpb)
protected abstract Constr	AbstractPBClauseCardConstrDataStructure.constructPB(int[] theLits, BigInteger[] coefs, BigInteger degree)
protected Constr	PuebloPBMinClauseCardConstrDataStructure.constructPB(int[] theLits, BigInteger[] coefs, BigInteger degree)
protected Constr	PBMaxClauseCardConstrDataStructure.constructPB(int[] theLits, BigInteger[] coefs, BigInteger degree)
Constr	AbstractPBDataStructureFactory.createCardinalityConstraint(IVecInt literals, int degree)
Constr	CompetResolutionPBMixedHTClauseCardConstrDataStructure.createClause(IVecInt literals)
Constr	AbstractPBDataStructureFactory.createClause(IVecInt literals)
Constr	CompetResolutionPBMixedWLClauseCardConstrDataStructure.createClause(IVecInt literals)
Constr	PuebloPBMinClauseCardConstrDataStructure.createClause(IVecInt literals)
Constr	AbstractPBDataStructureFactory.createPseudoBooleanConstraint(IVecInt literals, IVec<BigInteger> coefs, boolean moreThan, BigInteger degree)
Constr	AbstractPBDataStructureFactory.createUnregisteredClause(IVecInt literals)
Constr	AbstractPBDataStructureFactory.createUnregisteredPseudoBooleanConstraint(IDataStructurePB dspb)
protected abstract Constr	AbstractPBDataStructureFactory.learntConstraintFactory(IDataStructurePB dspb)
protected Constr	AbstractPBClauseCardConstrDataStructure.learntConstraintFactory(IDataStructurePB dspb)
protected Constr	PBMinDataStructure.learntConstraintFactory(IDataStructurePB dspb)

Uses of Constr in org.sat4j.pb.constraints.pb

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

interface

PBConstr

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

class	AtLeastPB
class	LearntBinaryClausePB
class	LearntHTClausePB
class	MaxWatchPb Data structure for pseudo-boolean constraint with watched literals.
class	MinWatchCardPB
class	MinWatchPb Data structure for pseudo-boolean constraint with watched literals.
class	MixableCBClausePB
class	OriginalBinaryClausePB
class	OriginalHTClausePB
class	PuebloMinWatchPb
class	UnitClausePB
class	WatchPb Abstract data structure for pseudo-boolean constraint with watched literals.

Uses of Constr in org.sat4j.pb.core

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

Constr	PBDataStructureFactory.createPseudoBooleanConstraint(IVecInt literals, IVec<BigInteger> coefs, boolean moreThan, BigInteger degree)
Constr	PBDataStructureFactory.createUnregisteredPseudoBooleanConstraint(IDataStructurePB dspb)

Methods in org.sat4j.pb.core with parameters of type Constr

void	PBSolverCP.analyze(Constr myconfl, Pair results)
void	PBSolverCP.analyzeCP(Constr myconfl, Pair results)