Uses of Interface
org.sat4j.specs.IConstr

Packages that use IConstr

org.sat4j.core	Implementation of the data structures available in org.sat4j.specs.
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.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.encoding
org.sat4j.tools.xplain	Implementation of an explanation engine in case of unsatisfiability.

Uses of IConstr in org.sat4j.core

Classes in org.sat4j.core 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.core that return IConstr

IConstr

ConstrGroup.getConstr(int i)

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

void	ConstrGroup.add(IConstr constr)

Uses of IConstr in org.sat4j.maxsat

Classes in org.sat4j.maxsat that implement IConstr

class

UnitWeightedClause

Methods in org.sat4j.maxsat that return IConstr

IConstr	WeightedMaxSatDecorator.addClause(IVecInt literals) Add a soft clause 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.addSoftAtLeast(BigInteger weight, IVecInt literals, int degree) Allow adding a new soft cardinality constraint in the solver.
IConstr	WeightedMaxSatDecorator.addSoftAtLeast(int weight, IVecInt literals, int degree) Allow adding a new soft cardinality constraint in the solver.
IConstr	WeightedMaxSatDecorator.addSoftAtLeast(IVecInt literals, int degree) Allow adding a new soft cardinality constraint in the solver.
IConstr	WeightedMaxSatDecorator.addSoftAtMost(BigInteger weight, IVecInt literals, int degree) Allow adding a new soft cardinality constraint in the solver.
IConstr	WeightedMaxSatDecorator.addSoftAtMost(int weight, IVecInt literals, int degree) Allow adding a new soft cardinality constraint in the solver.
IConstr	WeightedMaxSatDecorator.addSoftAtMost(IVecInt literals, int degree) Allow adding a new soft cardinality constraint in the solver.
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	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.

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.addExactly(IVecInt literals, int n)
IConstr	Solver.getIthConstr(int i) returns the ith constraint in the solver.

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

boolean	Solver.removeConstr(IConstr co)
boolean	Solver.removeSubsumedConstr(IConstr co)

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	PseudoBitsAdderDecorator.addAtLeast(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	IPBSolver.addAtLeast(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree) Create a pseudo-boolean constraint of the type "at least".
IConstr	UserFriendlyPBStringSolver.addAtLeast(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	PBSolverDecorator.addAtLeast(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	OPBStringSolver.addAtLeast(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	PseudoBitsAdderDecorator.addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
IConstr	IPBSolver.addAtLeast(IVecInt literals, IVecInt coeffs, int degree) Create a pseudo-boolean constraint of the type "at least".
IConstr	UserFriendlyPBStringSolver.addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
IConstr	PBSolverDecorator.addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
IConstr	OPBStringSolver.addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
IConstr	UserFriendlyPBStringSolver.addAtMost(IVecInt literals, int degree)
IConstr	OPBStringSolver.addAtMost(IVecInt literals, int degree)
IConstr	PseudoBitsAdderDecorator.addAtMost(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	IPBSolver.addAtMost(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree) Create a pseudo boolean constraint of the type "at most".
IConstr	UserFriendlyPBStringSolver.addAtMost(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	PBSolverDecorator.addAtMost(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	OPBStringSolver.addAtMost(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	PseudoBitsAdderDecorator.addAtMost(IVecInt literals, IVecInt coeffs, int degree)
IConstr	IPBSolver.addAtMost(IVecInt literals, IVecInt coeffs, int degree) Create a pseudo boolean constraint of the type "at most".
IConstr	UserFriendlyPBStringSolver.addAtMost(IVecInt literals, IVecInt coeffs, int degree)
IConstr	PBSolverDecorator.addAtMost(IVecInt literals, IVecInt coeffs, int degree)
IConstr	OPBStringSolver.addAtMost(IVecInt literals, IVecInt coeffs, int degree)
IConstr	UserFriendlyPBStringSolver.addClause(IVecInt literals)
IConstr	OPBStringSolver.addClause(IVecInt literals)
IConstr	PseudoBitsAdderDecorator.addExactly(IVecInt literals, IVec<BigInteger> coeffs, BigInteger weight)
IConstr	IPBSolver.addExactly(IVecInt literals, IVec<BigInteger> coeffs, BigInteger weight) Create a pseudo-boolean constraint of the type "subset sum".
IConstr	UserFriendlyPBStringSolver.addExactly(IVecInt literals, IVec<BigInteger> coeffs, BigInteger weight)
IConstr	PBSolverDecorator.addExactly(IVecInt literals, IVec<BigInteger> coeffs, BigInteger weight)
IConstr	OPBStringSolver.addExactly(IVecInt literals, IVec<BigInteger> coeffs, BigInteger weight)
IConstr	PseudoBitsAdderDecorator.addExactly(IVecInt literals, IVecInt coeffs, int weight)
IConstr	IPBSolver.addExactly(IVecInt literals, IVecInt coeffs, int weight) Create a pseudo-boolean constraint of the type "subset sum".
IConstr	UserFriendlyPBStringSolver.addExactly(IVecInt literals, IVecInt coeffs, int weight)
IConstr	PBSolverDecorator.addExactly(IVecInt literals, IVecInt coeffs, int weight)
IConstr	OPBStringSolver.addExactly(IVecInt literals, IVecInt coeffs, int weight)
IConstr	PseudoBitsAdderDecorator.addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d)
IConstr	IPBSolver.addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d) Create a Pseudo-Boolean constraint of the type "at least n or at most 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	IWatchPb
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	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 IConstr in org.sat4j.pb.core

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

IConstr	PBSolver.addAtLeast(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	PBSolver.addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
IConstr	PBSolver.addAtMost(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	PBSolver.addAtMost(IVecInt literals, IVecInt coeffs, int degree)
IConstr	PBSolver.addExactly(IVecInt literals, IVec<BigInteger> coeffs, BigInteger weight)
IConstr	PBSolver.addExactly(IVecInt literals, IVecInt coeffs, int weight)
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	ClausalConstraintsDecorator.addAtLeast(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	XplainPB.addAtLeast(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	ManyCorePB.addAtLeast(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	LexicoDecoratorPB.addAtLeast(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	ClausalConstraintsDecorator.addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
IConstr	XplainPB.addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
IConstr	ManyCorePB.addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
IConstr	LexicoDecoratorPB.addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
IConstr	XplainPB.addAtMost(IVecInt literals, int degree)
IConstr	ClausalConstraintsDecorator.addAtMost(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	XplainPB.addAtMost(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	ManyCorePB.addAtMost(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	LexicoDecoratorPB.addAtMost(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	ClausalConstraintsDecorator.addAtMost(IVecInt literals, IVecInt coeffs, int degree)
IConstr	XplainPB.addAtMost(IVecInt literals, IVecInt coeffs, int degree)
IConstr	ManyCorePB.addAtMost(IVecInt literals, IVecInt coeffs, int degree)
IConstr	LexicoDecoratorPB.addAtMost(IVecInt literals, IVecInt coeffs, int degree)
IConstr	XplainPB.addExactly(IVecInt literals, int n)
IConstr	ClausalConstraintsDecorator.addExactly(IVecInt literals, IVec<BigInteger> coeffs, BigInteger weight)
IConstr	XplainPB.addExactly(IVecInt literals, IVec<BigInteger> coeffs, BigInteger weight)
IConstr	ManyCorePB.addExactly(IVecInt literals, IVec<BigInteger> coeffs, BigInteger weight)
IConstr	LexicoDecoratorPB.addExactly(IVecInt literals, IVec<BigInteger> coeffs, BigInteger weight)
IConstr	ClausalConstraintsDecorator.addExactly(IVecInt literals, IVecInt coeffs, int weight)
IConstr	XplainPB.addExactly(IVecInt literals, IVecInt coeffs, int weight)
IConstr	ManyCorePB.addExactly(IVecInt literals, IVecInt coeffs, int weight)
IConstr	LexicoDecoratorPB.addExactly(IVecInt literals, IVecInt coeffs, int weight)
IConstr	ClausalConstraintsDecorator.addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d)
IConstr	XplainPB.addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d)
IConstr	ManyCorePB.addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d)
IConstr	LexicoDecoratorPB.addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d)
protected IConstr	LexicoDecoratorPB.discardSolutionsForOptimizing()

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.
IConstr	ISolver.addExactly(IVecInt literals, int n) Create a cardinality constraint of the type "exactly n of those literals must be satisfied".

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

Methods in org.sat4j.tools that return IConstr

IConstr	ManyCore.addAtLeast(IVecInt literals, int degree)
IConstr	ClausalCardinalitiesDecorator.addAtLeast(IVecInt literals, int k)
IConstr	DimacsOutputSolver.addAtLeast(IVecInt literals, int degree)
IConstr	DimacsStringSolver.addAtLeast(IVecInt literals, int degree)
IConstr	SolverDecorator.addAtLeast(IVecInt literals, int degree)
IConstr	ManyCore.addAtMost(IVecInt literals, int degree)
IConstr	ClausalCardinalitiesDecorator.addAtMost(IVecInt literals, int k)
IConstr	DimacsOutputSolver.addAtMost(IVecInt literals, int degree)
IConstr	DimacsStringSolver.addAtMost(IVecInt literals, int degree)
IConstr	SolverDecorator.addAtMost(IVecInt literals, int degree)
IConstr	AbstractOutputSolver.addBlockingClause(IVecInt literals)
IConstr	ManyCore.addBlockingClause(IVecInt literals)
IConstr	SolverDecorator.addBlockingClause(IVecInt literals)
IConstr	ManyCore.addClause(IVecInt literals)
IConstr	DimacsOutputSolver.addClause(IVecInt literals)
IConstr	DimacsStringSolver.addClause(IVecInt literals)
IConstr	SolverDecorator.addClause(IVecInt literals)
IConstr	ManyCore.addExactly(IVecInt literals, int n)
IConstr	ClausalCardinalitiesDecorator.addExactly(IVecInt literals, int k)
IConstr	DimacsOutputSolver.addExactly(IVecInt literals, int n)
IConstr	DimacsStringSolver.addExactly(IVecInt literals, int n)
IConstr	SolverDecorator.addExactly(IVecInt literals, int n)
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.
protected IConstr	LexicoDecorator.discardSolutionsForOptimizing()
IConstr	GateTranslator.gateFalse(int y) translate y <=> FALSE into a clause.
IConstr	GateTranslator.gateTrue(int y) translate y <=> TRUE into a clause.
IConstr[]	GateTranslator.halfOr(int y, IVecInt literals) translate y <= x1 \/ x2 \/ ... \/ xn into clauses.
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	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	AbstractOutputSolver.removeConstr(IConstr c)
boolean	ManyCore.removeConstr(IConstr c)
boolean	SolverDecorator.removeConstr(IConstr c)
boolean	AbstractOutputSolver.removeSubsumedConstr(IConstr c)
boolean	ManyCore.removeSubsumedConstr(IConstr c)
boolean	SolverDecorator.removeSubsumedConstr(IConstr c)

Uses of IConstr in org.sat4j.tools.encoding

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

IConstr	EncodingStrategyAdapter.addAtLeast(ISolver solver, IVecInt literals, int degree)
IConstr	EncodingStrategyAdapter.addAtLeastOne(ISolver solver, IVecInt literals)
IConstr	Sequential.addAtMost(ISolver solver, IVecInt literals, int k) This encoding adds (n-1)*k variables (n is the number of variables in the at most constraint and k is the degree of the constraint) and 2nk+n-3k-1 clauses.
IConstr	Policy.addAtMost(ISolver solver, IVecInt literals, int k)
IConstr	EncodingStrategyAdapter.addAtMost(ISolver solver, IVecInt literals, int degree)
IConstr	Product.addAtMost(ISolver solver, IVecInt literals, int k)
IConstr	Commander.addAtMost(ISolver solver, IVecInt literals, int degree)
IConstr	Binary.addAtMost(ISolver solver, IVecInt literals, int degree)
IConstr	Binomial.addAtMost(ISolver solver, IVecInt literals, int degree)
IConstr	Product.addAtMostNonOpt(ISolver solver, IVecInt literals, int k)
IConstr	Ladder.addAtMostOne(ISolver solver, IVecInt literals)
IConstr	EncodingStrategyAdapter.addAtMostOne(ISolver solver, IVecInt literals)
IConstr	Product.addAtMostOne(ISolver solver, IVecInt literals)
IConstr	Commander.addAtMostOne(ISolver solver, IVecInt literals) In this encoding, variables are partitioned in groups.
IConstr	Binary.addAtMostOne(ISolver solver, IVecInt literals) p being the smaller integer greater than log_2(n), this encoding adds p variables and n*p clauses.
IConstr	Binomial.addAtMostOne(ISolver solver, IVecInt literals)
IConstr	Policy.addExactly(ISolver solver, IVecInt literals, int n)
IConstr	EncodingStrategyAdapter.addExactly(ISolver solver, IVecInt literals, int degree)
IConstr	Ladder.addExactlyOne(ISolver solver, IVecInt literals)
IConstr	EncodingStrategyAdapter.addExactlyOne(ISolver solver, IVecInt literals)

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	HighLevelXplain.addAtLeast(IVecInt literals, int degree)
IConstr	Xplain.addAtMost(IVecInt literals, int degree)
IConstr	HighLevelXplain.addAtMost(IVecInt literals, int degree)
IConstr	Xplain.addClause(IVecInt literals)
IConstr	HighLevelXplain.addClause(IVecInt literals, int desc)
IConstr	Xplain.addExactly(IVecInt literals, int n)

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

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

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

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

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

Pair(Integer key, IConstr constr)