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	MixedDataStructureSingleWL.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	MixedDataStructureSingleWL.createClause(IVecInt literals)
Constr	CardinalityDataStructure.createClause(IVecInt literals)
Constr	MixedDataStructureDanielHT.createClause(IVecInt literals)
Constr	MixedDataStructureDanielWL.createClause(IVecInt literals)
Constr	CardinalityDataStructureYanMin.createClause(IVecInt literals)
Constr	CardinalityDataStructureYanMax.createClause(IVecInt literals)
Constr	ClausalDataStructureWL.createUnregisteredClause(IVecInt literals)
Constr	MixedDataStructureSingleWL.createUnregisteredClause(IVecInt literals)
Constr	CardinalityDataStructure.createUnregisteredClause(IVecInt literals)
Constr	MixedDataStructureDanielHT.createUnregisteredClause(IVecInt literals)
Constr	MixedDataStructureDanielWL.createUnregisteredClause(IVecInt literals)
Constr	CardinalityDataStructureYanMin.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)
static Constr	MaxWatchCard.maxWatchCardNew(UnitPropagationListener s, ILits voc, IVecInt ps, boolean moreThan, int degree) Permet la cr?
static Constr	MinWatchCard.minWatchCardNew(UnitPropagationListener s, ILits voc, IVecInt ps, boolean moreThan, int degree) Constructs a cardinality constraint with a minimal set of watched literals Permet la cr?

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

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) Create a cardinality constraint of the form sum li >= 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	AbstractPBClauseCardConstrDataStructure.constructCard(IVecInt theLits, int degree)
Constr	MinCardConstructor.constructCard(UnitPropagationListener solver, ILits voc, IVecInt theLits, int degree)
Constr	ICardConstructor.constructCard(UnitPropagationListener solver, ILits voc, IVecInt theLits, int degree)
Constr	AtLeastCardPBConstructor.constructCard(UnitPropagationListener solver, ILits voc, IVecInt theLits, int degree)
Constr	MinCardPBConstructor.constructCard(UnitPropagationListener solver, ILits voc, IVecInt theLits, int degree)
Constr	AtLeastCardConstructor.constructCard(UnitPropagationListener solver, ILits voc, IVecInt theLits, int degree)
protected Constr	AbstractPBClauseCardConstrDataStructure.constructClause(IVecInt v)
Constr	UnitBinaryHTClauseConstructor.constructClause(UnitPropagationListener solver, ILits voc, IVecInt v)
Constr	UnitBinaryWLClauseConstructor.constructClause(UnitPropagationListener solver, ILits voc, IVecInt v)
Constr	UnitBinaryHTClausePBConstructor.constructClause(UnitPropagationListener solver, ILits voc, IVecInt v)
Constr	IClauseConstructor.constructClause(UnitPropagationListener solver, ILits voc, IVecInt v)
protected Constr	AbstractPBClauseCardConstrDataStructure.constructLearntCard(IDataStructurePB dspb)
Constr	MinCardConstructor.constructLearntCard(ILits voc, IDataStructurePB dspb)
Constr	ICardConstructor.constructLearntCard(ILits voc, IDataStructurePB dspb)
Constr	AtLeastCardPBConstructor.constructLearntCard(ILits voc, IDataStructurePB dspb)
Constr	MinCardPBConstructor.constructLearntCard(ILits voc, IDataStructurePB dspb)
Constr	AtLeastCardConstructor.constructLearntCard(ILits voc, IDataStructurePB dspb)
Constr	UnitBinaryHTClauseConstructor.constructLearntClause(ILits voc, IVecInt literals)
Constr	UnitBinaryWLClauseConstructor.constructLearntClause(ILits voc, IVecInt literals)
Constr	UnitBinaryHTClausePBConstructor.constructLearntClause(ILits voc, IVecInt literals)
Constr	IClauseConstructor.constructLearntClause(ILits voc, IVecInt literals)
protected Constr	AbstractPBClauseCardConstrDataStructure.constructLearntClause(IVecInt literals)
protected Constr	AbstractPBClauseCardConstrDataStructure.constructLearntPB(IDataStructurePB dspb)
Constr	MinLongWatchPBConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
Constr	MaxLongWatchPBConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
Constr	MinWatchPBConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
Constr	MaxWatchPBConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
Constr	MinLongWatchPBCPConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
Constr	MaxLongWatchPBCPConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
Constr	IPBConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
Constr	PuebloMinWatchPBConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
protected Constr	AbstractPBClauseCardConstrDataStructure.constructPB(int[] theLits, BigInteger[] coefs, BigInteger degree)
Constr	MinLongWatchPBConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree)
Constr	MaxLongWatchPBConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree)
Constr	MinWatchPBConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree)
Constr	MaxWatchPBConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree)
Constr	MinLongWatchPBCPConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree)
Constr	MaxLongWatchPBCPConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree)
Constr	IPBConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree)
Constr	PuebloMinWatchPBConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree)
Constr	AbstractPBDataStructureFactory.createCardinalityConstraint(IVecInt literals, int degree)
Constr	AbstractPBDataStructureFactory.createClause(IVecInt literals)
Constr	AbstractPBClauseCardConstrDataStructure.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	AbstractPBClauseCardConstrDataStructure.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	IWatchPb
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	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 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)