org.sat4j.pb

Class PseudoOptDecorator

java.lang.Object

org.sat4j.tools.SolverDecorator<IPBSolver>

org.sat4j.pb.PBSolverDecorator

org.sat4j.pb.PseudoOptDecorator

All Implemented Interfaces:

Serializable, IPBSolver, IOptimizationProblem, IProblem, ISolver, RandomAccessModel

Direct Known Subclasses:

PseudoIteratorDecorator

public class PseudoOptDecorator
extends PBSolverDecorator
implements IOptimizationProblem

A decorator that computes minimal pseudo boolean models.

Author:

daniel

See Also:

Serialized Form

Constructor Summary

Constructors

Constructor and Description
PseudoOptDecorator(IPBSolver solver) Create a PB decorator for which a non optimal solution means that the problem is satisfiable.
PseudoOptDecorator(IPBSolver solver, boolean nonOptimalMeansSatisfiable) Create a PB decorator with a specific semantic of non optimal solution.
PseudoOptDecorator(IPBSolver solver, boolean nonOptimalMeansSatisfiable, boolean useAnImplicantForEvaluation) Create a PB decorator with a specific semantic of non optimal solution.

Method Summary

Methods

Modifier and Type	Method and Description
boolean	admitABetterSolution() Look for a solution of the optimization problem.
boolean	admitABetterSolution(IVecInt assumps) Look for a solution of the optimization problem when some literals are satisfied.
Number	calculateObjective() Compute the value of the objective function for the current solution.
void	discard() Discard the current solution in the optimization problem.
void	discardCurrentSolution() Discard the current solution in the optimization problem.
void	forceObjectiveValueTo(Number forcedValue) Force the value of the objective function.
Number	getObjectiveValue() Read only access to the value of the objective function for the current solution.
boolean	hasNoObjectiveFunction() If the optimization problem has no objective function, then it is a simple decision problem.
boolean	isOptimal() Allows to check afterwards if the solution provided by the solver is optimal or not.
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 assumps) Check the satisfiability of the set of constraints contained inside the solver.
boolean	isSatisfiable(IVecInt assumps, 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.
int[]	modelWithInternalVariables() That method is designed to be used to retrieve the real model of the current set of constraints, i.e. to provide the truth value of boolean variables used internally in the solver (for encoding purposes for instance).
boolean	nonOptimalMeansSatisfiable() A suboptimal solution has different meaning depending of the optimization problem considered.
void	reset() Clean up the internal state of the solver.
void	setObjectiveFunction(ObjectiveFunction objf) Provide an objective function to the solver.
void	setTimeout(int t) To set the internal timeout of the solver.
void	setTimeoutForFindingBetterSolution(int seconds) Allow to set a specific timeout when the solver is in optimization mode.
String	toString(String prefix) Display a textual representation of the solver configuration.

Methods inherited from class org.sat4j.pb.PBSolverDecorator

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

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, nConstraints, newVar, newVar, nextFreeVarId, nVars, primeImplicant, primeImplicant, printInfos, printInfos, printStat, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLogPrefix, setSearchListener, 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.IProblem

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

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, newVar, nextFreeVarId, printStat, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeoutMs, setTimeoutOnConflicts, setVerbose, unsatExplanation

Constructor Detail

PseudoOptDecorator

public PseudoOptDecorator(IPBSolver solver)

Create a PB decorator for which a non optimal solution means that the problem is satisfiable.

Parameters:

solver - a PB solver.

PseudoOptDecorator

public PseudoOptDecorator(IPBSolver solver,
                  boolean nonOptimalMeansSatisfiable)

Create a PB decorator with a specific semantic of non optimal solution.

Parameters:

solver - a PB solver

nonOptimalMeansSatisfiable - true if a suboptimal solution means that the problem is satisfiable (e.g. as in the PB competition), else false (e.g. as in the MAXSAT competition).

PseudoOptDecorator

public PseudoOptDecorator(IPBSolver solver,
                  boolean nonOptimalMeansSatisfiable,
                  boolean useAnImplicantForEvaluation)

Create a PB decorator with a specific semantic of non optimal solution.

Parameters:

solver - a PB solver

nonOptimalMeansSatisfiable - true if a suboptimal solution means that the problem is satisfiable (e.g. as in the PB competition), else false (e.g. as in the MAXSAT competition).

useAnImplicantForEvaluation - uses an implicant (a prime implicant computed using SolverDecorator.primeImplicant()) instead of a plain model to evaluate the objective function.

Method Detail

isSatisfiable

public boolean isSatisfiable()
                      throws TimeoutException

Description copied from interface: IProblem

Check the satisfiability of the set of constraints contained inside the solver.

Specified by:

isSatisfiable in interface IProblem

Overrides:

isSatisfiable in class SolverDecorator<IPBSolver>

Returns:

true if the set of constraints is satisfiable, else false.

Throws:

TimeoutException

isSatisfiable

public boolean isSatisfiable(boolean global)
                      throws TimeoutException

Description copied from interface: IProblem

Check the satisfiability of the set of constraints contained inside the solver.

Specified by:

isSatisfiable in interface IProblem

Overrides:

isSatisfiable in class SolverDecorator<IPBSolver>

Parameters:

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.

Returns:

true if the set of constraints is satisfiable, else false.

Throws:

TimeoutException

isSatisfiable

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

Description copied from interface: IProblem

Check the satisfiability of the set of constraints contained inside the solver.

Specified by:

isSatisfiable in interface IProblem

Overrides:

isSatisfiable in class SolverDecorator<IPBSolver>

Parameters:

assumps - 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.

Returns:

true if the set of constraints is satisfiable when literals are satisfied, else false.

Throws:

TimeoutException

isSatisfiable

public boolean isSatisfiable(IVecInt assumps)
                      throws TimeoutException

Description copied from interface: IProblem

Check the satisfiability of the set of constraints contained inside the solver.

Specified by:

isSatisfiable in interface IProblem

Overrides:

isSatisfiable in class SolverDecorator<IPBSolver>

Parameters:

assumps - a set of literals (represented by usual non null integers in Dimacs format).

Returns:

true if the set of constraints is satisfiable when literals are satisfied, else false.

Throws:

TimeoutException

setObjectiveFunction

public void setObjectiveFunction(ObjectiveFunction objf)

Description copied from interface: IPBSolver

Provide an objective function to the solver.

Specified by:

setObjectiveFunction in interface IPBSolver

Overrides:

setObjectiveFunction in class PBSolverDecorator

Parameters:

objf - the objective function

admitABetterSolution

public boolean admitABetterSolution()
                             throws TimeoutException

Description copied from interface: IOptimizationProblem

Look for a solution of the optimization problem.

Specified by:

admitABetterSolution in interface IOptimizationProblem

Returns:

true if a better solution than current one can be found.

Throws:

TimeoutException - if the solver cannot answer in reasonable time.

See Also:

ISolver.setTimeout(int)

admitABetterSolution

public boolean admitABetterSolution(IVecInt assumps)
                             throws TimeoutException

Description copied from interface: IOptimizationProblem

Look for a solution of the optimization problem when some literals are satisfied.

Specified by:

admitABetterSolution in interface IOptimizationProblem

Parameters:

assumps - a set of literals in Dimacs format.

Returns:

true if a better solution than current one can be found.

Throws:

TimeoutException - if the solver cannot answer in reasonable time.

See Also:

ISolver.setTimeout(int)

hasNoObjectiveFunction

public boolean hasNoObjectiveFunction()

Description copied from interface: IOptimizationProblem

If the optimization problem has no objective function, then it is a simple decision problem.

Specified by:

hasNoObjectiveFunction in interface IOptimizationProblem

Returns:

true if the problem is a decision problem, false if the problem is an optimization problem.

nonOptimalMeansSatisfiable

public boolean nonOptimalMeansSatisfiable()

Description copied from interface: IOptimizationProblem

A suboptimal solution has different meaning depending of the optimization problem considered. For instance, in the case of MAXSAT, a suboptimal solution does not mean that the problem is satisfiable, while in pseudo boolean optimization, it is true.

Specified by:

nonOptimalMeansSatisfiable in interface IOptimizationProblem

Returns:

true if founding a suboptimal solution means that the problem is satisfiable.

calculateObjective

public Number calculateObjective()

Description copied from interface: IOptimizationProblem

Compute the value of the objective function for the current solution. A call to that method only makes sense if hasNoObjectiveFunction()==false. DO NOT CALL THAT METHOD THAT WILL BE CALLED AUTOMATICALLY. USE getObjectiveValue() instead!

Specified by:

calculateObjective in interface IOptimizationProblem

Returns:

the value of the objective function.

See Also:

IOptimizationProblem.getObjectiveValue()

discardCurrentSolution

public void discardCurrentSolution()
                            throws ContradictionException

Description copied from interface: IOptimizationProblem

Discard the current solution in the optimization problem.

Specified by:

discardCurrentSolution in interface IOptimizationProblem

Throws:

ContradictionException - if a trivial inconsistency is detected.

reset

public void reset()

Description copied from interface: ISolver

Clean up the internal state of the solver. Note that such method should also be called when you no longer need the solver because the state of the solver may prevent the GC to proceed. There is a known issue for instance where failing to call reset() on a solver will keep timer threads alive and exhausts memory.

Specified by:

reset in interface ISolver

Overrides:

reset in class SolverDecorator<IPBSolver>

model

public int[] model()

Description copied from interface: IProblem

Provide a model (if any) for a satisfiable formula. That method should be called AFTER isSatisfiable() or isSatisfiable(IVecInt) if the formula is satisfiable. Else an exception UnsupportedOperationException is launched.

Specified by:

model in interface IProblem

Overrides:

model in class SolverDecorator<IPBSolver>

Returns:

a model of the formula as an array of literals to satisfy.

See Also:

IProblem.isSatisfiable(), IProblem.isSatisfiable(IVecInt)

model

public boolean model(int var)

Description copied from interface: RandomAccessModel

Provide the truth value of a specific variable in the model. That method should be called AFTER isSatisfiable() if the formula is satisfiable. Else an exception UnsupportedOperationException is launched.

Specified by:

model in interface RandomAccessModel

Overrides:

model in class SolverDecorator<IPBSolver>

Parameters:

var - the variable id in Dimacs format

Returns:

the truth value of that variable in the model

See Also:

#model()

toString

public String toString(String prefix)

Description copied from interface: ISolver

Display a textual representation of the solver configuration.

Specified by:

toString in interface ISolver

Overrides:

toString in class SolverDecorator<IPBSolver>

Parameters:

prefix - the prefix to use on each line.

Returns:

a textual description of the solver internals.

getObjectiveValue

public Number getObjectiveValue()

Description copied from interface: IOptimizationProblem

Read only access to the value of the objective function for the current solution.

Specified by:

getObjectiveValue in interface IOptimizationProblem

Returns:

the value of the objective function for the current solution.

discard

public void discard()
             throws ContradictionException

Description copied from interface: IOptimizationProblem

Discard the current solution in the optimization problem. THE NAME WAS NOT NICE. STILL AVAILABLE TO AVOID BREAKING THE API. PLEASE USE THE LONGER discardCurrentSolution() instead.

Specified by:

discard in interface IOptimizationProblem

Throws:

ContradictionException - if a trivial inconsistency is detected.

See Also:

IOptimizationProblem.discardCurrentSolution()

forceObjectiveValueTo

public void forceObjectiveValueTo(Number forcedValue)
                           throws ContradictionException

Description copied from interface: IOptimizationProblem

Force the value of the objective function. This is especially useful to iterate over optimal solutions.

Specified by:

forceObjectiveValueTo in interface IOptimizationProblem

Throws:

ContradictionException

isOptimal

public boolean isOptimal()

Description copied from interface: IOptimizationProblem

Allows to check afterwards if the solution provided by the solver is optimal or not.

Specified by:

isOptimal in interface IOptimizationProblem

Returns:

modelWithInternalVariables

public int[] modelWithInternalVariables()

Description copied from interface: ISolver

That method is designed to be used to retrieve the real model of the current set of constraints, i.e. to provide the truth value of boolean variables used internally in the solver (for encoding purposes for instance). If no variables are added in the solver, then Arrays.equals(model(),modelWithInternalVariables()). In case new variables are added to the solver, then the number of models returned by that method is greater of equal to the number of models returned by model() when using a ModelIterator.

Specified by:

modelWithInternalVariables in interface ISolver

Overrides:

modelWithInternalVariables in class SolverDecorator<IPBSolver>

Returns:

an array of literals, in Dimacs format, corresponding to a model of the formula over all the variables declared in the solver.

See Also:

IProblem.model(), ModelIterator

setTimeoutForFindingBetterSolution

public void setTimeoutForFindingBetterSolution(int seconds)

Description copied from interface: IOptimizationProblem

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

Specified by:

setTimeoutForFindingBetterSolution in interface IOptimizationProblem

setTimeout

public void setTimeout(int t)

Description copied from interface: ISolver

To set the internal timeout of the solver. When the timeout is reached, a timeout exception is launched by the solver.

Specified by:

setTimeout in interface ISolver

Overrides:

setTimeout in class SolverDecorator<IPBSolver>

Parameters:

t - the timeout (in s)