|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object org.sat4j.tools.SolverDecorator<T> org.sat4j.tools.xplain.Xplain<T>
T
- a subinterface to ISolver.public class Xplain<T extends ISolver>
An implementation of the QuickXplain algorithm as explained by Ulrich Junker in the following paper:
Field Summary | |
---|---|
protected IVecInt |
assump
|
protected Map<Integer,IConstr> |
constrs
|
Constructor Summary | |
---|---|
Xplain(T solver)
|
Method Summary | |
---|---|
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. |
void |
cancelExplanation()
|
protected int |
createNewVar(IVecInt literals)
|
protected void |
discardLastestVar()
|
Collection<IConstr> |
explain()
|
int[] |
findModel()
Look for a model satisfying all the clauses available in the problem. |
int[] |
findModel(IVecInt assumps)
Look for a model satisfying all the clauses available in the problem. |
Collection<IConstr> |
getConstraints()
|
boolean |
isSatisfiable()
Check the satisfiability of the set of constraints contained inside the solver. |
boolean |
isSatisfiable(boolean global)
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. |
boolean |
isSatisfiable(IVecInt assumps,
boolean global)
Check the satisfiability of the set of constraints contained inside the solver. |
int[] |
model()
Provide a model (if any) for a satisfiable formula. |
Methods inherited from class java.lang.Object |
---|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait |
Field Detail |
---|
protected Map<Integer,IConstr> constrs
protected IVecInt assump
Constructor Detail |
---|
public Xplain(T solver)
Method Detail |
---|
public IConstr addClause(IVecInt literals) throws ContradictionException
ISolver
addClause
in interface ISolver
addClause
in class SolverDecorator<T extends 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)
protected int createNewVar(IVecInt literals)
literals
-
protected void discardLastestVar()
public IConstr addAtLeast(IVecInt literals, int degree) throws ContradictionException
ISolver
addAtLeast
in interface ISolver
addAtLeast
in class SolverDecorator<T extends 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 addAtMost(IVecInt literals, int degree) throws ContradictionException
ISolver
addAtMost
in interface ISolver
addAtMost
in class SolverDecorator<T extends 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 Collection<IConstr> explain() throws TimeoutException
TimeoutException
public void cancelExplanation()
public Collection<IConstr> getConstraints()
public int[] findModel() throws TimeoutException
IProblem
if (isSatisfiable()) {
return model();
}
return null;
findModel
in interface IProblem
findModel
in class SolverDecorator<T extends ISolver>
null
if no model is found
TimeoutException
- if a model cannot be found within the given timeout.public int[] findModel(IVecInt assumps) throws TimeoutException
IProblem
if (isSatisfiable(assumpt)) {
return model();
}
return null;
findModel
in interface IProblem
findModel
in class SolverDecorator<T extends ISolver>
null
if no model is found
TimeoutException
- if a model cannot be found within the given timeout.public boolean isSatisfiable() throws TimeoutException
IProblem
isSatisfiable
in interface IProblem
isSatisfiable
in class SolverDecorator<T extends ISolver>
TimeoutException
public boolean isSatisfiable(boolean global) throws TimeoutException
IProblem
isSatisfiable
in interface IProblem
isSatisfiable
in class SolverDecorator<T extends ISolver>
global
- whether that call is part of a global process (i.e.
optimization) or not. if (global), the timeout will not be
reset between each call.
TimeoutException
public boolean isSatisfiable(IVecInt assumps) throws TimeoutException
IProblem
isSatisfiable
in interface IProblem
isSatisfiable
in class SolverDecorator<T extends ISolver>
assumps
- a set of literals (represented by usual non null integers
in Dimacs format).
TimeoutException
public boolean isSatisfiable(IVecInt assumps, boolean global) throws TimeoutException
IProblem
isSatisfiable
in interface IProblem
isSatisfiable
in class SolverDecorator<T extends ISolver>
assumps
- a set of literals (represented by usual non null integers
in Dimacs format).global
- whether that call is part of a global process (i.e.
optimization) or not. if (global), the timeout will not be
reset between each call.
TimeoutException
public int[] model()
IProblem
model
in interface IProblem
model
in class SolverDecorator<T extends ISolver>
IProblem.isSatisfiable()
,
IProblem.isSatisfiable(IVecInt)
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |