Uses of Interface
org.sat4j.specs.IConstr

Packages that use IConstr

org.sat4j.minisat.constraints.card	Implementations of cardinality constraints.
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.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.card

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

class	AtLeast Cardinality constraint.
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	BinaryClauses
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	MixableCBClause Counter Based clauses that can be mixed with WLCLauses
class	OriginalBinaryClause SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre All rights reserved.
class	OriginalHTClause
class	TernaryClauses
class	UnitClause

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.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	DecisionUIP.clauseNonAssertive(IConstr reason)
boolean	FirstUIP.clauseNonAssertive(IConstr reason)

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

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	DimacsStringSolver.addAtLeast(IVecInt literals, int degree)
IConstr	DimacsOutputSolver.addAtMost(IVecInt literals, int degree)
IConstr	SolverDecorator.addAtMost(IVecInt literals, int degree)
IConstr	DimacsStringSolver.addAtMost(IVecInt literals, int degree)
IConstr	DimacsOutputSolver.addClause(IVecInt literals)
IConstr	SolverDecorator.addClause(IVecInt literals)
IConstr	DimacsStringSolver.addClause(IVecInt literals)

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

void	ConstrGroup.add(IConstr constr)
boolean	DimacsOutputSolver.removeConstr(IConstr c)
boolean	SolverDecorator.removeConstr(IConstr c)
boolean	DimacsStringSolver.removeConstr(IConstr c)