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