Uses of Interface
org.sat4j.specs.IConstr

Packages that use IConstr

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.uip	Various ways to compute an asserting clause (containing one Unique Implication Point).
org.sat4j.opt	Built-in optimization framework.
org.sat4j.specs	Those classes are intented for users dealing with SAT solvers as blackboxes.
org.sat4j.tools	Tools to be used on top of an ISolver.

Uses of IConstr in org.sat4j.minisat.constraints

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

IConstr

AbstractPBDataStructureFactory.createUnregisteredPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)

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

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

class	AtLeast
class	MaxWatchCard
class	MinWatchCard

Uses of IConstr in org.sat4j.minisat.constraints.cnf

Classes in org.sat4j.minisat.constraints.cnf that implement IConstr

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.

Uses of IConstr in org.sat4j.minisat.constraints.pb

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

interface

PBConstr

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

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

Methods in org.sat4j.minisat.constraints.pb that return IConstr

IConstr	PBSolverWithImpliedClause.addPseudoBoolean(IVecInt literals, IVec<java.math.BigInteger> coeffs, boolean moreThan, java.math.BigInteger degree)
IConstr	IInternalPBConstraintCreator.createUnregisteredPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)

Uses of IConstr in org.sat4j.minisat.core

Subinterfaces of IConstr in org.sat4j.minisat.core

interface

Constr Basic constraint abstraction used in Solver.

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

IConstr	Solver.addAtLeast(IVecInt literals, int degree)
IConstr	Solver.addAtMost(IVecInt literals, int degree)
IConstr	Solver.addClause(IVecInt literals)
protected IConstr	Solver.addConstr(Constr constr)
IConstr	Solver.addPseudoBoolean(IVecInt literals, IVec<java.math.BigInteger> coeffs, boolean moreThan, java.math.BigInteger degree)
IConstr	Solver.getIthConstr(int i) returns the ith constraint in the solver.

Methods in org.sat4j.minisat.core with parameters of type IConstr

boolean	AssertingClauseGenerator.clauseNonAssertive(IConstr reason) method indicating if an asserting clause has been built. note that this method is called right after a resolution step is finished.
boolean	Solver.removeConstr(IConstr co)

Uses of IConstr in org.sat4j.minisat.uip

Methods in org.sat4j.minisat.uip with parameters of type IConstr

boolean	FirstUIP.clauseNonAssertive(IConstr reason)
boolean	DecisionUIP.clauseNonAssertive(IConstr reason)

Uses of IConstr in org.sat4j.opt

Methods in org.sat4j.opt that return IConstr

IConstr	MaxSatDecorator.addClause(IVecInt literals)
IConstr	WeightedMaxSatDecorator.addClause(IVecInt literals)

Uses of IConstr in org.sat4j.specs

Methods in org.sat4j.specs that return IConstr

IConstr	ISolver.addAtLeast(IVecInt literals, int degree) Create a cardinality constraint of the type "at least n of those literals must be satisfied"
IConstr	ISolver.addAtMost(IVecInt literals, int degree) Create a cardinality constraint of the type "at most n of those literals must be satisfied"
IConstr	ISolver.addClause(IVecInt literals) Create a clause from a set of literals The literals are represented by non null integers such that opposite literals a represented by opposite values.
IConstr	ISolver.addPseudoBoolean(IVecInt lits, IVec<java.math.BigInteger> coeffs, boolean moreThan, java.math.BigInteger d) Create a Pseudo-Boolean constraint of the type "at least n of those literals must be satisfied"

Methods in org.sat4j.specs with parameters of type IConstr

boolean

ISolver.removeConstr(IConstr c) Remove a constraint returned by one of the add method from the solver.

Uses of IConstr in org.sat4j.tools

Methods in org.sat4j.tools that return IConstr

IConstr	DimacsOutputSolver.addAtLeast(IVecInt literals, int degree)
IConstr	SolverDecorator.addAtLeast(IVecInt literals, int degree)
IConstr	DimacsOutputSolver.addAtMost(IVecInt literals, int degree)
IConstr	SolverDecorator.addAtMost(IVecInt literals, int degree)
IConstr	DimacsOutputSolver.addClause(IVecInt literals)
IConstr	SolverDecorator.addClause(IVecInt literals)
IConstr	DimacsOutputSolver.addPseudoBoolean(IVecInt lits, IVec<java.math.BigInteger> coeffs, boolean moreThan, java.math.BigInteger d)
IConstr	SolverDecorator.addPseudoBoolean(IVecInt literals, IVec<java.math.BigInteger> coeffs, boolean moreThan, java.math.BigInteger degree)

Methods in org.sat4j.tools with parameters of type IConstr

boolean	DimacsOutputSolver.removeConstr(IConstr c)
boolean	SolverDecorator.removeConstr(IConstr c)