|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectorg.sat4j.tools.SolverDecorator<IPBSolver>
org.sat4j.pb.PBSolverDecorator
org.sat4j.pb.OptToPBSATAdapter
public class OptToPBSATAdapter
Utility class to use optimization solvers instead of simple SAT solvers in code meant for SAT solvers.
Constructor Summary | |
---|---|
OptToPBSATAdapter(IOptimizationProblem problem)
|
Method Summary | |
---|---|
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 myAssumps)
Check the satisfiability of the set of constraints contained inside the solver. |
boolean |
isSatisfiable(IVecInt myAssumps,
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. |
boolean |
model(int var)
Provide the truth value of a specific variable in the model. |
String |
toString(String prefix)
Display a textual representation of the solver configuration. |
Methods inherited from class org.sat4j.pb.PBSolverDecorator |
---|
addPseudoBoolean, getObjectiveFunction, setObjectiveFunction |
Methods inherited from class java.lang.Object |
---|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait |
Methods inherited from interface org.sat4j.specs.ISolver |
---|
addAllClauses, addAtLeast, addAtMost, addBlockingClause, addClause, clearLearntClauses, expireTimeout, getLogPrefix, getSearchListener, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isVerbose, newVar, newVar, nextFreeVarId, printStat, printStat, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, unsatExplanation |
Methods inherited from interface org.sat4j.specs.IProblem |
---|
findModel, findModel, nConstraints, nVars, printInfos |
Constructor Detail |
---|
public OptToPBSATAdapter(IOptimizationProblem problem)
Method Detail |
---|
public boolean isSatisfiable() throws TimeoutException
IProblem
isSatisfiable
in interface IProblem
isSatisfiable
in class SolverDecorator<IPBSolver>
TimeoutException
public boolean isSatisfiable(boolean global) throws TimeoutException
IProblem
isSatisfiable
in interface IProblem
isSatisfiable
in class SolverDecorator<IPBSolver>
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 myAssumps, boolean global) throws TimeoutException
IProblem
isSatisfiable
in interface IProblem
isSatisfiable
in class SolverDecorator<IPBSolver>
myAssumps
- 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 boolean isSatisfiable(IVecInt myAssumps) throws TimeoutException
IProblem
isSatisfiable
in interface IProblem
isSatisfiable
in class SolverDecorator<IPBSolver>
myAssumps
- a set of literals (represented by usual non null integers
in Dimacs format).
TimeoutException
public int[] model()
IProblem
model
in interface IProblem
model
in class SolverDecorator<IPBSolver>
IProblem.isSatisfiable()
,
IProblem.isSatisfiable(IVecInt)
public boolean model(int var)
IProblem
model
in interface IProblem
model
in class SolverDecorator<IPBSolver>
var
- the variable id in Dimacs format
IProblem.model()
public String toString(String prefix)
ISolver
toString
in interface ISolver
toString
in class SolverDecorator<IPBSolver>
prefix
- the prefix to use on each line.
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |