public interface ISolver extends IProblem, java.io.Serializable
Modifier and Type | Method and Description |
---|---|
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 |
addBlockingClause(IVecInt literals)
Add a clause in order to prevent an assignment to occur.
|
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 |
addExactly(IVecInt literals,
int n)
Create a cardinality constraint of the type
"exactly n of those literals must be satisfied".
|
void |
clearLearntClauses()
Remove clauses learned during the solving process.
|
void |
expireTimeout()
Expire the timeout of the solver.
|
java.lang.String |
getLogPrefix() |
<S extends ISolverService> |
getSearchListener()
Get the current SearchListener.
|
ISolver |
getSolvingEngine()
Retrieve the real engine in case the engine is decorated by one or
several decorator.
|
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.
|
long |
getTimeoutMs()
Useful to check the internal timeout of the solver.
|
boolean |
isDBSimplificationAllowed()
Indicate whether the solver is allowed to simplify the formula by
propagating the truth value of top level satisfied variables.
|
boolean |
isSolverKeptHot()
Ask to the solver if it is in "hot" mode, meaning that the heuristics is
not reset after call is isSatisfiable().
|
boolean |
isVerbose()
To know if the solver is in verbose mode (output allowed) or not.
|
int[] |
modelWithInternalVariables()
That method is designed to be used to retrieve the real model of the
current set of constraints, i.e.
|
int |
newVar()
Deprecated.
|
int |
nextFreeVarId(boolean reserve)
Ask the solver for a free variable identifier, in Dimacs format (i.e.
|
void |
printStat(java.io.PrintStream out,
java.lang.String prefix)
Deprecated.
|
void |
printStat(java.io.PrintWriter out)
Display statistics to the given output writer
|
void |
printStat(java.io.PrintWriter out,
java.lang.String prefix)
Deprecated.
using the prefix does no longer makes sense because the
solver owns it.
|
int |
realNumberOfVariables()
Retrieve the real number of variables used in the solver.
|
void |
registerLiteral(int p)
Tell the solver to consider that the literal is in the CNF.
|
boolean |
removeConstr(IConstr c)
Remove a constraint returned by one of the add method from the solver.
|
boolean |
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.
|
void |
reset()
Clean up the internal state of the solver.
|
void |
setDBSimplificationAllowed(boolean status)
Set whether the solver is allowed to simplify the formula by propagating
the truth value of top level satisfied variables.
|
void |
setExpectedNumberOfClauses(int nb)
To inform the solver of the expected number of clauses to read.
|
void |
setKeepSolverHot(boolean keepHot)
Changed the behavior of the SAT solver heuristics between successive
calls.
|
void |
setLogPrefix(java.lang.String prefix)
Set the prefix used to display information.
|
<S extends ISolverService> |
setSearchListener(SearchListener<S> sl)
Allow the user to hook a listener to the solver to be notified of the
main steps of the search process.
|
void |
setTimeout(int t)
To set the internal timeout of the solver.
|
void |
setTimeoutMs(long t)
To set the internal timeout of the solver.
|
void |
setTimeoutOnConflicts(int count)
To set the internal timeout of the solver.
|
void |
setUnitClauseProvider(UnitClauseProvider ucp)
Allow the solver to ask for unit clauses before each restarts.
|
void |
setVerbose(boolean value)
Set the verbosity of the solver
|
java.lang.String |
toString(java.lang.String prefix)
Display a textual representation of the solver configuration.
|
IVecInt |
unsatExplanation()
Retrieve an explanation of the inconsistency in terms of assumption
literals.
|
findModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, nConstraints, newVar, nVars, primeImplicant, primeImplicant, printInfos, printInfos
model
@Deprecated int newVar()
int nextFreeVarId(boolean reserve)
realNumberOfVariables()
method.reserve
- if true, the maxVarId is updated in the solver, i.e.
successive calls to nextFreeVarId(true) will return increasing
variable id while successive calls to nextFreeVarId(false)
will always answer the same.realNumberOfVariables()
void registerLiteral(int p)
p
- the literal in Dimacs format that should appear in the model.void setExpectedNumberOfClauses(int nb)
p cnf
line is
read in dimacs formatted input file.
Note that this method is supposed to be called AFTER a call to
newVar(int)nb
- the expected number of clauses.IProblem.newVar(int)
IConstr addClause(IVecInt literals) throws ContradictionException
literals
- a set of literalsContradictionException
- iff the vector of literals is empty or if it contains only
falsified literals after unit propagationremoveConstr(IConstr)
IConstr addBlockingClause(IVecInt literals) throws ContradictionException
literals
- ContradictionException
boolean removeConstr(IConstr c)
c
- a constraint returned by one of the add method.boolean removeSubsumedConstr(IConstr c)
c
- a constraint returned by one of the add method. It must be the
latest constr added to the solver.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 (n) of the cardinality constraintContradictionException
- 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 (n) of the cardinality constraintContradictionException
- iff the vector of literals is empty or if degree literals are
not remaining unfalsified after unit propagationremoveConstr(IConstr)
IConstr addExactly(IVecInt literals, int n) 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.n
- the number of literals that must be satisfiedContradictionException
- iff the constraint is trivially unsatisfiable.void setTimeout(int t)
t
- the timeout (in s)void setTimeoutOnConflicts(int count)
count
- the timeout (in number of conflicts)void setTimeoutMs(long t)
t
- the timeout (in milliseconds)int getTimeout()
long getTimeoutMs()
void expireTimeout()
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)
@Deprecated void printStat(java.io.PrintWriter out, java.lang.String prefix)
out
- prefix
- the prefix to put in front of each linevoid printStat(java.io.PrintWriter out)
out
- setLogPrefix(String)
java.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.void clearLearntClauses()
void setDBSimplificationAllowed(boolean status)
boolean isDBSimplificationAllowed()
<S extends ISolverService> void setSearchListener(SearchListener<S> sl)
sl
- a Search Listener.void setUnitClauseProvider(UnitClauseProvider ucp)
ucp
- an object able to provide unit clauses.<S extends ISolverService> SearchListener<S> getSearchListener()
boolean isVerbose()
void setVerbose(boolean value)
value
- true to allow the solver to output messages on the console,
false either.void setLogPrefix(java.lang.String prefix)
prefix
- the prefix to be in front of each line of textjava.lang.String getLogPrefix()
IVecInt unsatExplanation()
IProblem.isSatisfiable(IVecInt)
,
IProblem.isSatisfiable(IVecInt, boolean)
int[] modelWithInternalVariables()
IProblem.model()
,
ModelIterator
int realNumberOfVariables()
nextFreeVarId(boolean)
method.nextFreeVarId(boolean)
boolean isSolverKeptHot()
void setKeepSolverHot(boolean keepHot)
keepHot
- true to keep the heuristics values across calls, false either.ISolver getSolvingEngine()