

PREV CLASS NEXT CLASS  FRAMES NO FRAMES  
SUMMARY: NESTED  FIELD  CONSTR  METHOD  DETAIL: FIELD  CONSTR  METHOD 
public interface ISolver
That interface contains all the services available on a SAT 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 lits,
IVec<java.math.BigInteger> coeffs,
boolean moreThan,
java.math.BigInteger d)
Create a PseudoBoolean constraint of the type "at least n of those literals must be satisfied" 
java.util.Map<java.lang.String,java.lang.Number> 
getStat()
To obtain a map of the available statistics from the solver. 
int 
getTimeout()
Useful to check the internal timeout of 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). 
void 
printStat(java.io.PrintStream out,
java.lang.String prefix)
Deprecated. 
void 
printStat(java.io.PrintWriter out,
java.lang.String prefix)
Display statistics to the given output writer 
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 
setExpectedNumberOfClauses(int nb)
To inform the solver of the expected number of clauses to read. 
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 interface org.sat4j.specs.IProblem 

isSatisfiable, isSatisfiable, model, model, nConstraints, nVars 
Method Detail 

int newVar()
int newVar(int howmany)
howmany
variables in the solver (and thus in the
vocabulary).
howmany
 number of variables to create
void setExpectedNumberOfClauses(int nb)
p cnf
line is read in dimacs formatted input file.
nb
 the expected number of clauses.IConstr addClause(IVecInt literals) throws ContradictionException
literals
 a set of literals
ContradictionException
 iff the vector of literals is empty or if it contains
only falsified literals after unit propagationremoveConstr(IConstr)
boolean removeConstr(IConstr c)
c
 a constraint returned by one of the add method.
void addAllClauses(IVec<IVecInt> clauses) throws ContradictionException
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 propagationaddClause(IVecInt)
IConstr addAtMost(IVecInt literals, int degree) throws ContradictionException
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 propagationremoveConstr(IConstr)
IConstr addAtLeast(IVecInt literals, int degree) throws ContradictionException
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 propagationremoveConstr(IConstr)
IConstr addPseudoBoolean(IVecInt lits, IVec<java.math.BigInteger> coeffs, boolean moreThan, java.math.BigInteger d) throws ContradictionException
lits
 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 >= degreed
 the degree of the cardinality constraint
ContradictionException
 iff the vector of literals is empty or if the constraint
is falsified after unit propagationremoveConstr(IConstr)
void setTimeout(int t)
t
 the timeout (in s)int getTimeout()
void reset()
@Deprecated void printStat(java.io.PrintStream out, java.lang.String prefix)
out
 prefix
 the prefix to put in front of each lineprintStat(PrintWriter, String)
void printStat(java.io.PrintWriter out, java.lang.String prefix)
out
 prefix
 the prefix to put in front of each linejava.util.Map<java.lang.String,java.lang.Number> getStat()
java.lang.String toString(java.lang.String prefix)
prefix
 the prefix to use on each line.


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