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 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	MixedDataStructureDaniel.createCardinalityConstraint(IVecInt literals, int degree)
Constr	CardinalityDataStructure.createCardinalityConstraint(IVecInt literals, int degree)
Constr	AbstractDataStructureFactory.createCardinalityConstraint(IVecInt literals, int degree)
Constr	MixedDataStructureDanielCBHT.createClause(IVecInt literals)
Constr	MixedDataStructureDaniel.createClause(IVecInt literals)
Constr	ClausalDataStructureHT.createClause(IVecInt literals)
Constr	CardinalityDataStructure.createClause(IVecInt literals)
Constr	MixedDataStructureWithBinaryAndTernary.createClause(IVecInt literals)
Constr	ClausalDataStructureCBHT.createClause(IVecInt literals)
Constr	MixedDataStructureWithBinary.createClause(IVecInt literals)
Constr	ClausalDataStructureCB.createClause(IVecInt literals)
Constr	MixedDataStructureDaniel.createUnregisteredClause(IVecInt literals)
Constr	ClausalDataStructureHT.createUnregisteredClause(IVecInt literals)
Constr	CardinalityDataStructure.createUnregisteredClause(IVecInt literals)
Constr	MixedDataStructureWithBinaryAndTernary.createUnregisteredClause(IVecInt literals)
Constr	ClausalDataStructureCBHT.createUnregisteredClause(IVecInt literals)
Constr	MixedDataStructureWithBinary.createUnregisteredClause(IVecInt literals)
Constr	ClausalDataStructureCB.createUnregisteredClause(IVecInt literals)

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

void	AbstractDataStructureFactory.learnConstraint(Constr constr)
void	MixedDataStructureWithBinaryAndTernary.learnConstraint(Constr constr)
void	MixedDataStructureWithBinary.learnConstraint(Constr constr)

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

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

class	AtLeast Cardinality constraint.
class	MinWatchCard

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	BinaryClauses
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	MixableCBClause Counter Based clauses that can be mixed with WLCLauses
class	OriginalBinaryClause SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre All rights reserved.
class	OriginalHTClause
class	TernaryClauses
class	UnitClause

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

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