org.sat4j.pb
Class OptToPBSATAdapter

java.lang.Object
  org.sat4j.tools.SolverDecorator<IPBSolver>
      org.sat4j.pb.PBSolverDecorator
          org.sat4j.pb.OptToPBSATAdapter

All Implemented Interfaces:

Serializable, IPBSolver, IProblem, ISolver

public class OptToPBSATAdapter
extends PBSolverDecorator

Utility class to use optimization solvers instead of simple SAT solvers in code meant for SAT solvers.

Author:

daniel

See Also:

Serialized Form

Constructor Summary

OptToPBSATAdapter(IOptimizationProblem problem)

Method Summary

boolean	isOptimal()
boolean	isSatisfiable()
boolean	isSatisfiable(boolean global)
boolean	isSatisfiable(IVecInt myAssumps)
boolean	isSatisfiable(IVecInt myAssumps, boolean global)
int[]	model()
boolean	model(int var)
String	toString(String prefix)

Methods inherited from class org.sat4j.pb.PBSolverDecorator

addAtLeast, addAtLeast, addAtMost, addAtMost, addExactly, addExactly, addPseudoBoolean, getObjectiveFunction, setObjectiveFunction

Methods inherited from class org.sat4j.tools.SolverDecorator

addAllClauses, addAtLeast, addAtMost, addBlockingClause, addClause, addExactly, clearDecorated, clearLearntClauses, decorated, expireTimeout, findModel, findModel, getLogPrefix, getSearchListener, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isVerbose, modelWithInternalVariables, nConstraints, newVar, newVar, nextFreeVarId, nVars, primeImplicant, printInfos, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, toString, unsatExplanation

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, addExactly, clearLearntClauses, expireTimeout, getLogPrefix, getSearchListener, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isVerbose, modelWithInternalVariables, newVar, nextFreeVarId, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, unsatExplanation

Methods inherited from interface org.sat4j.specs.IProblem

findModel, findModel, nConstraints, newVar, nVars, primeImplicant, printInfos

Constructor Detail

OptToPBSATAdapter

public OptToPBSATAdapter(IOptimizationProblem problem)

Method Detail

isSatisfiable

public boolean isSatisfiable()
                      throws TimeoutException

Specified by:

isSatisfiable in interface IProblem

Overrides:

isSatisfiable in class SolverDecorator<IPBSolver>

Throws:

TimeoutException

isSatisfiable

public boolean isSatisfiable(boolean global)
                      throws TimeoutException

Specified by:

isSatisfiable in interface IProblem

Overrides:

isSatisfiable in class SolverDecorator<IPBSolver>

Throws:

TimeoutException

isSatisfiable

public boolean isSatisfiable(IVecInt myAssumps,
                             boolean global)
                      throws TimeoutException

Specified by:

isSatisfiable in interface IProblem

Overrides:

isSatisfiable in class SolverDecorator<IPBSolver>

Throws:

TimeoutException

isSatisfiable

public boolean isSatisfiable(IVecInt myAssumps)
                      throws TimeoutException

Specified by:

isSatisfiable in interface IProblem

Overrides:

isSatisfiable in class SolverDecorator<IPBSolver>

Throws:

TimeoutException

model

public int[] model()

Specified by:

model in interface IProblem

Overrides:

model in class SolverDecorator<IPBSolver>

model

public boolean model(int var)

Specified by:

model in interface IProblem

Overrides:

model in class SolverDecorator<IPBSolver>

toString

public String toString(String prefix)

Specified by:

toString in interface ISolver

Overrides:

toString in class SolverDecorator<IPBSolver>

isOptimal

public boolean isOptimal()