

PREV CLASS NEXT CLASS  FRAMES NO FRAMES  
SUMMARY: NESTED  FIELD  CONSTR  METHOD  DETAIL: FIELD  CONSTR  METHOD 
java.lang.Object org.sat4j.tools.SolverDecorator
public abstract class SolverDecorator
The aim of that class is to allow adding dynamic responsabilities to SAT solvers using the Decorator design pattern. The class is abstract because it does not makes sense to use it "as is".
Constructor Summary  

SolverDecorator(ISolver solver)

Method Summary  

void 
addAllClauses(IVec<IVecInt> clauses)
Create clauses from a set of set of literals. 
IConstr 
addAtLeast(IVecInt literals,
int degree)
Create a cardinality constraint of the type "at least n of those literals must be satisfied" 
IConstr 
addAtMost(IVecInt literals,
int degree)
Create a cardinality constraint of the type "at most n of those literals must be satisfied" 
IConstr 
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 
addPseudoBoolean(IVecInt literals,
IVec<java.math.BigInteger> coeffs,
boolean moreThan,
java.math.BigInteger degree)
Create a PseudoBoolean constraint of the type "at least n of those literals must be satisfied" 
ISolver 
decorated()

int 
getTimeout()
Useful to check the internal timeout of the solver. 
boolean 
isSatisfiable()
Check the satisfiability of the set of constraints contained inside the solver. 
boolean 
isSatisfiable(IVecInt assumps)
Check the satisfiability of the set of constraints contained inside the solver. 
int[] 
model()
Provide a model (if any) for a satisfiable formula. 
int 
nConstraints()
To know the number of constraints currently available in the solver. 
int 
newVar()
Create a new variable in the solver (and thus in the vocabulary). 
int 
newVar(int howmany)
Create howmany variables in the solver (and thus in the
vocabulary). 
int 
nVars()
To know the number of variables used in the solver. 
void 
printStat(java.io.PrintStream out,
java.lang.String prefix)
Display statistics to the given output stream 
boolean 
removeConstr(IConstr c)
Remove a constraint returned by one of the add method from the solver. 
void 
reset()
Clean up the internal state of the solver. 
void 
setTimeout(int t)
To set the internal timeout of the solver. 
java.lang.String 
toString(java.lang.String prefix)
Display a textual representation of the solver configuration. 
Methods inherited from class java.lang.Object 

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait 
Constructor Detail 

public SolverDecorator(ISolver solver)
Method Detail 

public int getTimeout()
ISolver
getTimeout
in interface ISolver
public java.lang.String toString(java.lang.String prefix)
ISolver
toString
in interface ISolver
prefix
 the prefix to use on each line.
public void printStat(java.io.PrintStream out, java.lang.String prefix)
ISolver
printStat
in interface ISolver
prefix
 the prefix to put in front of each linepublic int newVar()
ISolver
newVar
in interface ISolver
public int newVar(int howmany)
ISolver
howmany
variables in the solver (and thus in the
vocabulary).
newVar
in interface ISolver
howmany
 number of variables to create
public IConstr addClause(IVecInt literals) throws ContradictionException
ISolver
addClause
in interface ISolver
literals
 a set of literals
ContradictionException
 iff the vector of literals is empty or if it contains
only falsified literals after unit propagationISolver.removeConstr(IConstr)
public void addAllClauses(IVec<IVecInt> clauses) throws ContradictionException
ISolver
addAllClauses
in interface ISolver
clauses
 a vector of set (VecInt) of literals in the dimacs format.
The vector can be reused since the solver is not supposed
to keep a reference to that vector.
ContradictionException
 iff the vector of literals is empty or if it contains
only falsified literals after unit propagationISolver.addClause(IVecInt)
public IConstr addAtMost(IVecInt literals, int degree) throws ContradictionException
ISolver
addAtMost
in interface ISolver
literals
 a set of literals
The vector can be reused since the solver is not supposed
to keep a reference to that vector.degree
 the degree of the cardinality constraint
ContradictionException
 iff the vector of literals is empty or if it contains
more than degree satisfied literals after unit propagationISolver.removeConstr(IConstr)
public IConstr addAtLeast(IVecInt literals, int degree) throws ContradictionException
ISolver
addAtLeast
in interface ISolver
literals
 a set of literals.
The vector can be reused since the solver is not supposed
to keep a reference to that vector.degree
 the degree of the cardinality constraint
ContradictionException
 iff the vector of literals is empty or if degree literals are not
remaining unfalsified after unit propagationISolver.removeConstr(IConstr)
public IConstr addPseudoBoolean(IVecInt literals, IVec<java.math.BigInteger> coeffs, boolean moreThan, java.math.BigInteger degree) throws ContradictionException
ISolver
addPseudoBoolean
in interface ISolver
literals
 a set of literals.
The vector can be reused since the solver is not supposed
to keep a reference to that vector.coeffs
 the coefficients of the literals.
The vector can be reused since the solver is not supposed
to keep a reference to that vector.moreThan
 true if it is a constraint >= degreedegree
 the degree of the cardinality constraint
ContradictionException
 iff the vector of literals is empty or if the constraint
is falsified after unit propagationISolver.removeConstr(IConstr)
public int[] model()
IProblem
model
in interface IProblem
public boolean isSatisfiable() throws TimeoutException
IProblem
isSatisfiable
in interface IProblem
TimeoutException
public boolean isSatisfiable(IVecInt assumps) throws TimeoutException
IProblem
isSatisfiable
in interface IProblem
assumps
 a set of literals (represented by usual non null integers in
Dimacs format).
TimeoutException
public void setTimeout(int t)
ISolver
setTimeout
in interface ISolver
t
 the timeout (in s)public int nConstraints()
IProblem
nConstraints
in interface IProblem
public int nVars()
IProblem
nVars
in interface IProblem
public void reset()
ISolver
reset
in interface ISolver
public ISolver decorated()
public boolean removeConstr(IConstr c)
ISolver
removeConstr
in interface ISolver
c
 a constraint returned by one of the add method.


PREV CLASS NEXT CLASS  FRAMES NO FRAMES  
SUMMARY: NESTED  FIELD  CONSTR  METHOD  DETAIL: FIELD  CONSTR  METHOD 