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

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.
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, isSolverKeptHot, isVerbose, modelWithInternalVariables, nConstraints, newVar, newVar, nextFreeVarId, nVars, primeImplicant, primeImplicant, printInfos, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, 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, isSolverKeptHot, isVerbose, modelWithInternalVariables, newVar, nextFreeVarId, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, unsatExplanation

Methods inherited from interface org.sat4j.specs.IProblem

findModel, findModel, nConstraints, newVar, nVars, primeImplicant, 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 int[] model(PrintWriter out)

Compute a minimal model according to the objective function of the IPBProblem decorated.

Parameters:

out - a writer to display information in verbose mode

Since:

2.3.2

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()

getCurrentObjectiveValue

public Number getCurrentObjectiveValue()

Return the value of the objective function in the last model found.

Returns:

Since:

2.3.2