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, RandomAccessModel

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

Constructors

Constructor and Description
OptToPBSATAdapter(IOptimizationProblem problem)
OptToPBSATAdapter(IOptimizationProblem problem, SolutionFoundListener sfl)

Method Summary

Methods

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	setSolutionFoundListener(SolutionFoundListener sfl)
void	setTimeoutForFindingBetterSolution(int seconds) Allow to set a specific timeout when the solver is in optimization mode.
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, 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, setUnitClauseProvider, 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, 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, setUnitClauseProvider, setVerbose, unsatExplanation

Methods inherited from interface org.sat4j.specs.IProblem

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

Constructor Detail

OptToPBSATAdapter

public OptToPBSATAdapter(IOptimizationProblem problem)

OptToPBSATAdapter

public OptToPBSATAdapter(IOptimizationProblem problem,
                 SolutionFoundListener sfl)

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 RandomAccessModel

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

setTimeoutForFindingBetterSolution

public void setTimeoutForFindingBetterSolution(int seconds)

Allow to set a specific timeout when the solver is in optimization mode. The solver internal timeout will be set to that value once it has found a solution. That way, the original timeout of the solver may be reduced if the solver finds quickly a solution, or increased if the solver finds regularly new solutions (thus giving more time to the solver each time).

See Also:

IOptimizationProblem.setTimeoutForFindingBetterSolution(int)

setSolutionFoundListener

public void setSolutionFoundListener(SolutionFoundListener sfl)