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 constraints.
org.sat4j.minisat.constraints.cnf	Implementations of clausal constraints.
org.sat4j.minisat.core	Implementation of the MiniSAT solver skeleton.
org.sat4j.minisat.learning	Various learning strategies.
org.sat4j.minisat.restarts	Various restart strategies.
org.sat4j.pb.constraints	Implementation of data structures for pseudo boolean constraints.
org.sat4j.pb.constraints.pb	Implementations of pseudo boolean constraints.
org.sat4j.pb.core	Implementations of pseudo boolean solvers
org.sat4j.sat	Implementation of a sat4j Launcher.

Uses of Constr in org.sat4j.minisat.constraints

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

Constr	MixedDataStructureSingleWL.createCardinalityConstraint(IVecInt literals, int degree)
Constr	MixedDataStructureDanielWL.createCardinalityConstraint(IVecInt literals, int degree)
Constr	MixedDataStructureDanielHT.createCardinalityConstraint(IVecInt literals, int degree)
Constr	CardinalityDataStructureYanMin.createCardinalityConstraint(IVecInt literals, int degree)
Constr	CardinalityDataStructureYanMax.createCardinalityConstraint(IVecInt literals, int degree)
Constr	CardinalityDataStructure.createCardinalityConstraint(IVecInt literals, int degree)
Constr	AbstractDataStructureFactory.createCardinalityConstraint(IVecInt literals, int degree)
Constr	MixedDataStructureSingleWL.createClause(IVecInt literals)
Constr	MixedDataStructureDanielWL.createClause(IVecInt literals)
Constr	MixedDataStructureDanielHT.createClause(IVecInt literals)
Constr	ClausalDataStructureWL.createClause(IVecInt literals)
Constr	CardinalityDataStructureYanMin.createClause(IVecInt literals)
Constr	CardinalityDataStructureYanMax.createClause(IVecInt literals)
Constr	CardinalityDataStructure.createClause(IVecInt literals)
Constr	MixedDataStructureSingleWL.createUnregisteredClause(IVecInt literals)
Constr	MixedDataStructureDanielWL.createUnregisteredClause(IVecInt literals)
Constr	MixedDataStructureDanielHT.createUnregisteredClause(IVecInt literals)
Constr	ClausalDataStructureWL.createUnregisteredClause(IVecInt literals)
Constr	CardinalityDataStructureYanMin.createUnregisteredClause(IVecInt literals)
Constr	CardinalityDataStructureYanMax.createUnregisteredClause(IVecInt literals)
Constr	CardinalityDataStructure.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?
Constr	MinWatchCard.toConstraint()
Constr	MaxWatchCard.toConstraint()
Constr	AtLeast.toConstraint()

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)
Constr	WLClause.toConstraint()
Constr	HTClause.toConstraint()
Constr	BinaryClause.toConstraint()

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

Fields in org.sat4j.minisat.core with type parameters of type Constr

protected IVec<Constr>	Solver.constrs Set of original constraints.
protected IVec<Constr>	Solver.learnts Set of learned constraints.

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) Returns the reason of the assignment of a literal.
Constr	Solver.propagate()
Constr	Propagatable.toConstraint() Allow to access a constraint view of the propagatable to avoid casting.

Methods in org.sat4j.minisat.core that return types with arguments of type Constr

IVec<Constr>

Solver.getLearnedConstraints()

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
int	ActivityComparator.compare(Constr c1, Constr c2)
boolean	UnitPropagationListener.enqueue(int p, Constr from) satisfies a literal
boolean	Solver.enqueue(int p, Constr from)
void	Solver.learn(Constr c)
void	Learner.learn(Constr c)
void	DataStructureFactory.learnConstraint(Constr constr)
void	LearningStrategy.learns(Constr constr)
void	RestartStrategy.newLearnedClause(Constr learned, int trailLevel)
void	LearnedConstraintsDeletionStrategy.onClauseLearning(Constr outLearnt) Hook method called when a new clause has just been derived during conflict analysis.
void	LearnedConstraintsDeletionStrategy.onConflictAnalysis(Constr reason) Hook method called on constraints participating to the conflict analysis.
void	LearnedConstraintsDeletionStrategy.onPropagation(Constr from) Hook method called when a unit clause is propagated thanks to from.
void	ILits.setReason(int lit, Constr r) Sets the reason of the assignment of a literal.

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

void	LearnedConstraintsDeletionStrategy.reduce(IVec<Constr> learnedConstrs) Hook method called when the solver wants to reduce the set of learned clauses.

Uses of Constr in org.sat4j.minisat.learning

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

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

Uses of Constr in org.sat4j.minisat.restarts

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

void	NoRestarts.newLearnedClause(Constr learned, int trailLevel)
void	MiniSATRestarts.newLearnedClause(Constr learned, int trailLevel)
void	LubyRestarts.newLearnedClause(Constr learned, int trailLevel)
void	ArminRestarts.newLearnedClause(Constr learned, int trailLevel)

Uses of Constr in org.sat4j.pb.constraints

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

protected Constr	PBMaxDataStructure.constraintFactory(int[] literals, BigInteger[] coefs, BigInteger degree)
protected abstract Constr	AbstractPBDataStructureFactory.constraintFactory(int[] literals, BigInteger[] coefs, BigInteger degree)
protected Constr	AbstractPBClauseCardConstrDataStructure.constraintFactory(int[] literals, BigInteger[] coefs, BigInteger degree)
protected Constr	AbstractPBClauseCardConstrDataStructure.constructCard(IVecInt theLits, int degree)
Constr	MinCardPBConstructor.constructCard(UnitPropagationListener solver, ILits voc, 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	AtLeastCardConstructor.constructCard(UnitPropagationListener solver, ILits voc, IVecInt theLits, int degree)
protected Constr	AbstractPBClauseCardConstrDataStructure.constructClause(IVecInt v)
Constr	UnitBinaryWLClauseConstructor.constructClause(UnitPropagationListener solver, ILits voc, IVecInt v)
Constr	UnitBinaryHTClausePBConstructor.constructClause(UnitPropagationListener solver, ILits voc, IVecInt v)
Constr	UnitBinaryHTClauseConstructor.constructClause(UnitPropagationListener solver, ILits voc, IVecInt v)
Constr	IClauseConstructor.constructClause(UnitPropagationListener solver, ILits voc, IVecInt v)
protected Constr	AbstractPBClauseCardConstrDataStructure.constructLearntCard(IDataStructurePB dspb)
Constr	MinCardPBConstructor.constructLearntCard(ILits voc, IDataStructurePB dspb)
Constr	MinCardConstructor.constructLearntCard(ILits voc, IDataStructurePB dspb)
Constr	ICardConstructor.constructLearntCard(ILits voc, IDataStructurePB dspb)
Constr	AtLeastCardPBConstructor.constructLearntCard(ILits voc, IDataStructurePB dspb)
Constr	AtLeastCardConstructor.constructLearntCard(ILits voc, IDataStructurePB dspb)
Constr	UnitBinaryWLClauseConstructor.constructLearntClause(ILits voc, IVecInt literals)
Constr	UnitBinaryHTClausePBConstructor.constructLearntClause(ILits voc, IVecInt literals)
Constr	UnitBinaryHTClauseConstructor.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	PuebloMinWatchPBConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
Constr	MinWatchPBConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
Constr	MinLongWatchPBCPConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
Constr	MinLongWatchPBConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
Constr	MaxWatchPBConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
Constr	MaxLongWatchPBCPConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
Constr	MaxLongWatchPBConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
Constr	IPBConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
protected Constr	AbstractPBClauseCardConstrDataStructure.constructPB(int[] theLits, BigInteger[] coefs, BigInteger degree)
Constr	PuebloMinWatchPBConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs)
Constr	MinWatchPBConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs)
Constr	MinLongWatchPBCPConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs)
Constr	MinLongWatchPBConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs)
Constr	MaxWatchPBConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs)
Constr	MaxLongWatchPBCPConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs)
Constr	MaxLongWatchPBConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs)
Constr	IPBConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs)
Constr	AbstractPBDataStructureFactory.createAtLeastPBConstraint(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)
Constr	AbstractPBDataStructureFactory.createAtMostPBConstraint(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)
Constr	AbstractPBDataStructureFactory.createCardinalityConstraint(IVecInt literals, int degree)
Constr	PuebloPBMinClauseCardConstrDataStructure.createClause(IVecInt literals)
Constr	AbstractPBDataStructureFactory.createClause(IVecInt literals)
Constr	AbstractPBClauseCardConstrDataStructure.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 Constr	PBMinDataStructure.learntConstraintFactory(IDataStructurePB dspb)
protected abstract Constr	AbstractPBDataStructureFactory.learntConstraintFactory(IDataStructurePB dspb)
protected Constr	AbstractPBClauseCardConstrDataStructure.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

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

Constr	WatchPbLongCP.toConstraint()
Constr	WatchPbLong.toConstraint()
Constr	WatchPb.toConstraint()

Uses of Constr in org.sat4j.pb.core

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

Constr	PBDataStructureFactory.createAtLeastPBConstraint(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)
Constr	PBDataStructureFactory.createAtMostPBConstraint(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)
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)

Uses of Constr in org.sat4j.sat

Methods in org.sat4j.sat with parameters of type Constr

void	RemoteControlStrategy.newLearnedClause(Constr learned, int trailLevel)