Uses of Interface
org.sat4j.specs.IConstr

Packages that use IConstr

Package	Description
org.sat4j.core	Implementation of the data structures available in org.sat4j.specs.
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.opt	Built-in optimization framework.
org.sat4j.specs	Those classes are intended for users dealing with SAT solvers as black boxes.
org.sat4j.tools	Tools to be used on top of an ISolver.
org.sat4j.tools.encoding	Implementation of different encodings.
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

Modifier and Type	Class and Description
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

Modifier and Type	Method and Description
IConstr	ConstrGroup.getConstr(int i)

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

Modifier and Type	Method and Description
void	ConstrGroup.add(IConstr constr)

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

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

Modifier and Type	Class and Description
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

Modifier and Type	Class and Description
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

Modifier and Type	Interface and Description
interface	Constr Basic constraint abstraction used in Solver.

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

Modifier and Type	Method and Description
IConstr	Solver.addAtLeast(IVecInt literals, int degree)
IConstr	Solver.addAtMost(IVecInt literals, int degree)
IConstr	Solver.addAtMostOnTheFly(int[] literals, int degree)
IConstr	Solver.addBlockingClause(IVecInt literals)
IConstr	Solver.addClause(IVecInt literals)
IConstr	Solver.addClauseOnTheFly(int[] 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

Modifier and Type	Method and Description
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

Modifier and Type	Method and Description
IConstr	MaxSatDecorator.addClause(IVecInt literals)

Uses of IConstr in org.sat4j.specs

Methods in org.sat4j.specs that return IConstr

Modifier and Type	Method and Description
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	ISolverService.addAtMostOnTheFly(int[] literals, int degree) Add a new pseudo cardinality constraint sum literals <= degree in the solver.
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	IGroupSolver.addClause(IVecInt literals, int desc)
IConstr	ISolverService.addClauseOnTheFly(int[] literals) Add a new clause in the SAT solver.
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 that return types with arguments of type IConstr

Modifier and Type	Method and Description
IVec<? extends IConstr>	ISolverService.getLearnedConstraints() Read-Only access to the list of constraints learned and not deleted so far in the solver.

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

Modifier and Type	Method and Description
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	ISolverService.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.
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

Modifier and Type	Method and Description
IConstr	NegationDecorator.addAtLeast(IVecInt literals, int degree)
IConstr	ManyCore.addAtLeast(IVecInt literals, int degree)
IConstr	ClausalCardinalitiesDecorator.addAtLeast(IVecInt literals, int k)
IConstr	DimacsOutputSolver.addAtLeast(IVecInt literals, int degree)
IConstr	StatisticsSolver.addAtLeast(IVecInt literals, int degree)
IConstr	DimacsStringSolver.addAtLeast(IVecInt literals, int degree)
IConstr	SolverDecorator.addAtLeast(IVecInt literals, int degree)
IConstr	NegationDecorator.addAtMost(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	StatisticsSolver.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	StatisticsSolver.addBlockingClause(IVecInt literals)
IConstr	SolverDecorator.addBlockingClause(IVecInt literals)
IConstr	NegationDecorator.addClause(IVecInt literals)
IConstr	ManyCore.addClause(IVecInt literals)
IConstr	FullClauseSelectorSolver.addClause(IVecInt literals)
IConstr	DimacsOutputSolver.addClause(IVecInt literals)
IConstr	StatisticsSolver.addClause(IVecInt literals)
IConstr	DimacsStringSolver.addClause(IVecInt literals)
IConstr	SolverDecorator.addClause(IVecInt literals)
IConstr	GroupClauseSelectorSolver.addClause(IVecInt literals, int desc)
IConstr	FullClauseSelectorSolver.addControlableClause(IVecInt literals)
IConstr	GroupClauseSelectorSolver.addControlableClause(IVecInt literals, int desc)
IConstr	NegationDecorator.addExactly(IVecInt literals, int n)
IConstr	ManyCore.addExactly(IVecInt literals, int n)
IConstr	ClausalCardinalitiesDecorator.addExactly(IVecInt literals, int k)
IConstr	DimacsOutputSolver.addExactly(IVecInt literals, int n)
IConstr	StatisticsSolver.addExactly(IVecInt literals, int n)
IConstr	DimacsStringSolver.addExactly(IVecInt literals, int n)
IConstr	SolverDecorator.addExactly(IVecInt literals, int n)
IConstr	FullClauseSelectorSolver.addNonControlableClause(IVecInt literals)
IConstr	GroupClauseSelectorSolver.addNonControlableClause(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.
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	FullClauseSelectorSolver.getLastConstr()
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 that return types with arguments of type IConstr

Modifier and Type	Method and Description
Collection<IConstr>	FullClauseSelectorSolver.getConstraints()
Map<Integer,IConstr>	FullClauseSelectorSolver.getConstrs()

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

Modifier and Type	Method and Description
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	SearchListenerAdapter.conflictFound(IConstr confl, int dlevel, int trailLevel)
void	LBDTracing.conflictFound(IConstr confl, int dlevel, int trailLevel)
void	MultiTracing.conflictFound(IConstr confl, int dlevel, int trailLevel)
void	DecisionLevelTracing.conflictFound(IConstr confl, int dlevel, int trailLevel)
void	ConflictDepthTracing.conflictFound(IConstr confl, int dlevel, int trailLevel)
void	ConflictLevelTracing.conflictFound(IConstr confl, int dlevel, int trailLevel)
void	TextOutputTracing.learn(IConstr clause)
void	DotSearchTracing.learn(IConstr clause)
void	SearchListenerAdapter.learn(IConstr c)
void	MultiTracing.learn(IConstr c)
void	LearnedClausesSizeTracing.learn(IConstr c)
void	TextOutputTracing.propagating(int p, IConstr reason)
void	DotSearchTracing.propagating(int p, IConstr reason)
void	SearchListenerAdapter.propagating(int p, IConstr reason)
void	SpeedTracing.propagating(int p, IConstr reason)
void	MultiTracing.propagating(int p, IConstr reason)
boolean	AbstractOutputSolver.removeConstr(IConstr c)
boolean	ManyCore.removeConstr(IConstr c)
boolean	StatisticsSolver.removeConstr(IConstr c)
boolean	SolverDecorator.removeConstr(IConstr c)
boolean	AbstractOutputSolver.removeSubsumedConstr(IConstr c)
boolean	ManyCore.removeSubsumedConstr(IConstr c)
boolean	StatisticsSolver.removeSubsumedConstr(IConstr c)
boolean	SolverDecorator.removeSubsumedConstr(IConstr c)
void	FullClauseSelectorSolver.setLastConstr(IConstr lastConstr)

Uses of IConstr in org.sat4j.tools.encoding

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

Modifier and Type	Method and Description
IConstr	Policy.addAtLeast(ISolver solver, IVecInt literals, int n)
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 k)
IConstr	Binomial.addAtMost(ISolver solver, IVecInt literals, int degree)
IConstr	Product.addAtMostNonOpt(ISolver solver, IVecInt literals, int k)
IConstr	Sequential.addAtMostOne(ISolver solver, IVecInt literals)
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	Sequential.addExactly(ISolver solver, IVecInt literals, int degree)
IConstr	Policy.addExactly(ISolver solver, IVecInt literals, int n)
IConstr	EncodingStrategyAdapter.addExactly(ISolver solver, IVecInt literals, int degree)
IConstr	Product.addExactly(ISolver solver, IVecInt literals, int degree)
IConstr	Commander.addExactly(ISolver solver, IVecInt literals, int degree)
IConstr	Binary.addExactly(ISolver solver, IVecInt literals, int degree)
IConstr	Binomial.addExactly(ISolver solver, IVecInt literals, int degree)
IConstr	Sequential.addExactlyOne(ISolver solver, IVecInt literals)
IConstr	Ladder.addExactlyOne(ISolver solver, IVecInt literals)
IConstr	EncodingStrategyAdapter.addExactlyOne(ISolver solver, IVecInt literals)
IConstr	Product.addExactlyOne(ISolver solver, IVecInt literals)
IConstr	Commander.addExactlyOne(ISolver solver, IVecInt literals)
IConstr	Binary.addExactlyOne(ISolver solver, IVecInt literals)
IConstr	Binomial.addExactlyOne(ISolver solver, IVecInt literals)

Uses of IConstr in org.sat4j.tools.xplain

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

Modifier and Type	Method and Description
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.addExactly(IVecInt literals, int n)

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

Modifier and Type	Method and Description
Collection<IConstr>	Xplain.explain() Provide an explanation of the inconsistency in term of a subset minimal set of constraints.

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

Modifier and Type	Method and Description
boolean	Xplain.removeConstr(IConstr c)
boolean	Xplain.removeSubsumedConstr(IConstr c)