public class OptToPBSATAdapter extends PBSolverDecorator
Constructor and Description |
---|
OptToPBSATAdapter(IOptimizationProblem problem) |
Modifier and Type | Method and Description |
---|---|
Number |
getCurrentObjectiveValue()
Return the value of the objective function in the last model found.
|
boolean |
isOptimal() |
boolean |
isSatisfiable() |
boolean |
isSatisfiable(boolean global) |
boolean |
isSatisfiable(IVecInt myAssumps) |
boolean |
isSatisfiable(IVecInt myAssumps,
boolean global) |
int[] |
model() |
boolean |
model(int var) |
int[] |
model(PrintWriter out)
Compute a minimal model according to the objective function of the
IPBProblem decorated.
|
void |
setTimeoutForFindingBetterSolution(int seconds)
Allow to set a specific timeout when the solver is in optimization mode.
|
String |
toString(String prefix) |
addAtLeast, addAtLeast, addAtMost, addAtMost, addExactly, addExactly, addPseudoBoolean, getObjectiveFunction, setObjectiveFunction
addAllClauses, addAtLeast, addAtMost, addBlockingClause, addClause, addExactly, clearDecorated, clearLearntClauses, decorated, expireTimeout, findModel, findModel, getLogPrefix, getSearchListener, getSolvingEngine, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSolverKeptHot, isVerbose, modelWithInternalVariables, nConstraints, newVar, newVar, nextFreeVarId, nVars, primeImplicant, primeImplicant, printInfos, printInfos, printStat, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, toString, unsatExplanation
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
addAllClauses, addAtLeast, addAtMost, addBlockingClause, addClause, addExactly, clearLearntClauses, expireTimeout, getLogPrefix, getSearchListener, getSolvingEngine, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSolverKeptHot, isVerbose, modelWithInternalVariables, newVar, nextFreeVarId, printStat, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, unsatExplanation
findModel, findModel, nConstraints, newVar, nVars, primeImplicant, primeImplicant, printInfos, printInfos
public OptToPBSATAdapter(IOptimizationProblem problem)
public boolean isSatisfiable() throws TimeoutException
isSatisfiable
in interface IProblem
isSatisfiable
in class SolverDecorator<IPBSolver>
TimeoutException
public boolean isSatisfiable(boolean global) throws TimeoutException
isSatisfiable
in interface IProblem
isSatisfiable
in class SolverDecorator<IPBSolver>
TimeoutException
public boolean isSatisfiable(IVecInt myAssumps, boolean global) throws TimeoutException
isSatisfiable
in interface IProblem
isSatisfiable
in class SolverDecorator<IPBSolver>
TimeoutException
public boolean isSatisfiable(IVecInt myAssumps) throws TimeoutException
isSatisfiable
in interface IProblem
isSatisfiable
in class SolverDecorator<IPBSolver>
TimeoutException
public int[] model()
model
in interface IProblem
model
in class SolverDecorator<IPBSolver>
public int[] model(PrintWriter out)
out
- a writer to display information in verbose modepublic boolean model(int var)
model
in interface RandomAccessModel
model
in class SolverDecorator<IPBSolver>
public String toString(String prefix)
toString
in interface ISolver
toString
in class SolverDecorator<IPBSolver>
public boolean isOptimal()
public Number getCurrentObjectiveValue()
public void setTimeoutForFindingBetterSolution(int seconds)
Copyright © 2013 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.