Uses of Interface
org.sat4j.specs.IConstr

Packages that use IConstr

org.sat4j.maxsat	MAXSAT and Weighted Max SAT framework.
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.uip	Various ways to compute an asserting clause (containing one Unique Implication Point).
org.sat4j.multicore
org.sat4j.opt	Built-in optimization framework.
org.sat4j.pb
org.sat4j.pb.constraints.pb	Implementations of pseudo boolean contraints.
org.sat4j.pb.core
org.sat4j.pb.tools
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.
org.sat4j.tools.xplain

Uses of IConstr in org.sat4j.maxsat

Methods in org.sat4j.maxsat that return IConstr

IConstr	WeightedMaxSatDecorator.addClause(IVecInt literals) Add a set of literals to the solver.
IConstr	WeightedMaxSatDecorator.addHardClause(IVecInt literals) Add a hard clause in the solver, i.e. a clause that must be satisfied.
IConstr	WeightedMaxSatDecorator.addSoftClause(BigInteger weight, IVecInt literals)
IConstr	WeightedMaxSatDecorator.addSoftClause(int weight, IVecInt literals) Add a soft clause to the solver.
IConstr	WeightedMaxSatDecorator.addSoftClause(IVecInt literals) Add a soft clause in the solver, i.e. a clause with a weight of 1.

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

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.addBlockingClause(IVecInt literals)
IConstr	Solver.addClause(IVecInt literals)
protected IConstr	Solver.addConstr(Constr constr)
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)
boolean	Solver.removeSubsumedConstr(IConstr co)

Uses of IConstr in org.sat4j.minisat.uip

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

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

Uses of IConstr in org.sat4j.multicore

Methods in org.sat4j.multicore that return IConstr

IConstr	ManyCore.addAtLeast(IVecInt literals, int degree)
IConstr	ManyCore.addAtMost(IVecInt literals, int degree)
IConstr	ManyCore.addBlockingClause(IVecInt literals)
IConstr	ManyCore.addClause(IVecInt literals)
IConstr	ManyCorePB.addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d)

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

boolean	ManyCore.removeConstr(IConstr c)
boolean	ManyCore.removeSubsumedConstr(IConstr c)

Uses of IConstr in org.sat4j.opt

Methods in org.sat4j.opt that return IConstr

IConstr

MaxSatDecorator.addClause(IVecInt literals)

Uses of IConstr in org.sat4j.pb

Methods in org.sat4j.pb that return IConstr

IConstr	UserFriendlyPBStringSolver.addAtLeast(IVecInt literals, int degree)
IConstr	OPBStringSolver.addAtLeast(IVecInt literals, int degree)
IConstr	UserFriendlyPBStringSolver.addAtMost(IVecInt literals, int degree)
IConstr	OPBStringSolver.addAtMost(IVecInt literals, int degree)
IConstr	UserFriendlyPBStringSolver.addClause(IVecInt literals)
IConstr	OPBStringSolver.addClause(IVecInt literals)
IConstr	IPBSolver.addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d) Create a Pseudo-Boolean constraint of the type "at least n of those literals must be satisfied"
IConstr	UserFriendlyPBStringSolver.addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d)
IConstr	PBSolverDecorator.addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d)
IConstr	OPBStringSolver.addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d)

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

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

interface

PBConstr

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

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 IConstr in org.sat4j.pb.core

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

IConstr	PBSolver.addPseudoBoolean(IVecInt literals, IVec<BigInteger> coeffs, boolean moreThan, BigInteger degree)
IConstr	PBSolverWithImpliedClause.addPseudoBoolean(IVecInt literals, IVec<BigInteger> coeffs, boolean moreThan, BigInteger degree)

Uses of IConstr in org.sat4j.pb.tools

Methods in org.sat4j.pb.tools that return IConstr

IConstr	XplainPB.addAtLeast(IVecInt literals, int degree)
IConstr	XplainPB.addAtMost(IVecInt literals, int degree)
IConstr	XplainPB.addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d)

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

void	ConflictTracing.conflictFound(IConstr confl, int dlevel, int trailLevel)
void	ConflictTracing.learn(IConstr c)
void	ConflictTracing.propagating(int p, IConstr reason)

Constructor parameters in org.sat4j.pb.tools with type arguments of type IConstr

ImplicationNamer(DependencyHelper<T,C> helper, IVec<IConstr> toName)

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.addBlockingClause(IVecInt literals) Add a clause in order to prevent an assignment to occur.
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.

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

void	SearchListener.conflictFound(IConstr confl, int dlevel, int trailLevel) a conflict has been found.
void	SearchListener.learn(IConstr c) learning a new clause
void	SearchListener.propagating(int p, IConstr reason) Unit propagation
boolean	ISolver.removeConstr(IConstr c) Remove a constraint returned by one of the add method from the solver.
boolean	ISolver.removeSubsumedConstr(IConstr c) Remove a constraint returned by one of the add method from the solver that is subsumed by a constraint already in the solver or to be added to the solver.

Uses of IConstr in org.sat4j.tools

Classes in org.sat4j.tools that implement IConstr

class

ConstrGroup A utility class used to manage easily group of clauses to be deleted at some point in the solver.

Methods in org.sat4j.tools that return IConstr

IConstr	DimacsOutputSolver.addAtLeast(IVecInt literals, int degree)
IConstr	DimacsStringSolver.addAtLeast(IVecInt literals, int degree)
IConstr	SolverDecorator.addAtLeast(IVecInt literals, int degree)
IConstr	DimacsOutputSolver.addAtMost(IVecInt literals, int degree)
IConstr	DimacsStringSolver.addAtMost(IVecInt literals, int degree)
IConstr	SolverDecorator.addAtMost(IVecInt literals, int degree)
IConstr	DimacsOutputSolver.addBlockingClause(IVecInt literals)
IConstr	DimacsStringSolver.addBlockingClause(IVecInt literals)
IConstr	SolverDecorator.addBlockingClause(IVecInt literals)
IConstr	DimacsOutputSolver.addClause(IVecInt literals)
IConstr	DimacsStringSolver.addClause(IVecInt literals)
IConstr	SolverDecorator.addClause(IVecInt literals)
IConstr[]	GateTranslator.and(int y, int x1, int x2) Translate y <=> x1 /\ x2
IConstr[]	GateTranslator.and(int y, IVecInt literals) Translate y <=> x1 /\ x2 /\ ... /\ xn into clauses.
IConstr	GateTranslator.gateFalse(int y) translate y <=> FALSE into a clause.
IConstr	GateTranslator.gateTrue(int y) translate y <=> TRUE into a clause.
IConstr	ConstrGroup.getConstr(int i)
IConstr[]	GateTranslator.iff(int y, IVecInt literals) translate y <=> (x1 <=> x2 <=> ... <=> xn) into clauses.
IConstr[]	GateTranslator.ite(int y, int x1, int x2, int x3) translate y <=> if x1 then x2 else x3 into clauses.
IConstr[]	GateTranslator.not(int y, int x) Translate y <=> not x into clauses.
IConstr[]	GateTranslator.or(int y, IVecInt literals) translate y <=> x1 \/ x2 \/ ... \/ xn into clauses.
IConstr[]	GateTranslator.xor(int y, IVecInt literals) translate y <=> x1 xor x2 xor ... xor xn into clauses.

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

void	ConstrGroup.add(IConstr constr)
void	TextOutputTracing.conflictFound(IConstr confl, int dlevel, int trailLevel)
void	LearnedClauseSizeTracing.conflictFound(IConstr confl, int dlevel, int trailLevel)
void	DotSearchTracing.conflictFound(IConstr confl, int dlevel, int trailLevel)
void	DecisionTracing.conflictFound(IConstr confl, int dlevel, int trailLevel)
void	DecisionLevelTracing.conflictFound(IConstr confl, int dlevel, int trailLevel)
void	ConflictLevelTracing.conflictFound(IConstr confl, int dlevel, int trailLevel)
void	TextOutputTracing.learn(IConstr clause)
void	LearnedClauseSizeTracing.learn(IConstr c)
void	DotSearchTracing.learn(IConstr clause)
void	DecisionTracing.learn(IConstr c)
void	DecisionLevelTracing.learn(IConstr c)
void	ConflictLevelTracing.learn(IConstr c)
void	TextOutputTracing.propagating(int p, IConstr reason)
void	LearnedClauseSizeTracing.propagating(int p, IConstr reason)
void	DotSearchTracing.propagating(int p, IConstr reason)
void	DecisionTracing.propagating(int p, IConstr reason)
void	DecisionLevelTracing.propagating(int p, IConstr reason)
void	ConflictLevelTracing.propagating(int p, IConstr reason)
boolean	DimacsOutputSolver.removeConstr(IConstr c)
boolean	DimacsStringSolver.removeConstr(IConstr c)
boolean	SolverDecorator.removeConstr(IConstr c)
boolean	DimacsOutputSolver.removeSubsumedConstr(IConstr c)
boolean	DimacsStringSolver.removeSubsumedConstr(IConstr c)
boolean	SolverDecorator.removeSubsumedConstr(IConstr c)

Uses of IConstr in org.sat4j.tools.xplain

Fields in org.sat4j.tools.xplain declared as IConstr

IConstr

Pair.constr

Fields in org.sat4j.tools.xplain with type parameters of type IConstr

protected Map<Integer,IConstr>

Xplain.constrs

Methods in org.sat4j.tools.xplain that return IConstr

IConstr	Xplain.addAtLeast(IVecInt literals, int degree)
IConstr	Xplain.addAtMost(IVecInt literals, int degree)
IConstr	Xplain.addClause(IVecInt literals)

Methods in org.sat4j.tools.xplain that return types with arguments of type IConstr

Collection<IConstr>	Xplain.explain()
Collection<IConstr>	Xplain.getConstraints()

Method parameters in org.sat4j.tools.xplain with type arguments of type IConstr

IVecInt	QuickXplainStrategy.explain(ISolver solver, Map<Integer,IConstr> constrs, IVecInt assumps)
IVecInt	ReplayXplainStrategy.explain(ISolver solver, Map<Integer,IConstr> constrs, IVecInt assumps)
IVecInt	XplainStrategy.explain(ISolver solver, Map<Integer,IConstr> constrs, IVecInt assumps)

Constructors in org.sat4j.tools.xplain with parameters of type IConstr

Pair(Integer key, IConstr constr)