org.sat4j.specs

Interface IOptimizationProblem

All Superinterfaces:

IProblem, RandomAccessModel

All Known Implementing Classes:

AbstractSelectorVariablesDecorator, LexicoDecorator, MaxSatDecorator, MinOneDecorator

public interface IOptimizationProblem
extends IProblem

Represents an optimization problem. The SAT solver will find suboptimal solutions of the problem until no more solutions are available. The latest solution found will be the optimal one. Such kind of problem is supposed to be handled:

 boolean isSatisfiable = false;
 
 IOptimizationProblem optproblem = (IOptimizationProblem) problem;
 
 try {
     while (optproblem.admitABetterSolution()) {
         if (!isSatisfiable) {
             if (optproblem.nonOptimalMeansSatisfiable()) {
                 setExitCode(ExitCode.SATISFIABLE);
                 if (optproblem.hasNoObjectiveFunction()) {
                     return;
                 }
                 log("SATISFIABLE"); //$NON-NLS-1$
             }
             isSatisfiable = true;
             log("OPTIMIZING..."); //$NON-NLS-1$
         }
         log("Got one! Elapsed wall clock time (in seconds):" //$NON-NLS-1$
                 + (System.currentTimeMillis() - getBeginTime()) / 1000.0);
         getLogWriter().println(
                 CURRENT_OPTIMUM_VALUE_PREFIX + optproblem.getObjectiveValue());
         optproblem.discardCurrentSolution();
     }
     if (isSatisfiable) {
         setExitCode(ExitCode.OPTIMUM_FOUND);
     } else {
         setExitCode(ExitCode.UNSATISFIABLE);
     }
 } catch (ContradictionException ex) {
     assert isSatisfiable;
     setExitCode(ExitCode.OPTIMUM_FOUND);
 }
 

Author:

leberre

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() Deprecated.
void	discard() Deprecated.
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	nonOptimalMeansSatisfiable() A suboptimal solution has different meaning depending of the optimization problem considered.
void	setTimeoutForFindingBetterSolution(int seconds) Allow to set a specific timeout when the solver is in optimization mode.

Methods inherited from interface org.sat4j.specs.IProblem

findModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, nConstraints, newVar, nVars, primeImplicant, primeImplicant, printInfos, printInfos

Methods inherited from interface org.sat4j.specs.RandomAccessModel

model

Method Detail

admitABetterSolution

boolean admitABetterSolution()
                             throws TimeoutException

Look for a solution of the optimization problem.

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

boolean admitABetterSolution(IVecInt assumps)
                             throws TimeoutException

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

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.

Since:

2.1

See Also:

ISolver.setTimeout(int)

hasNoObjectiveFunction

boolean hasNoObjectiveFunction()

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

Returns:

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

nonOptimalMeansSatisfiable

boolean nonOptimalMeansSatisfiable()

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.

Returns:

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

calculateObjective

@Deprecated
Number calculateObjective()

Deprecated.

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!

Returns:

the value of the objective function.

See Also:

getObjectiveValue()

getObjectiveValue

Number getObjectiveValue()

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

Returns:

the value of the objective function for the current solution.

Since:

2.1

forceObjectiveValueTo

void forceObjectiveValueTo(Number forcedValue)
                           throws ContradictionException

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

Throws:

ContradictionException

Since:

2.1

discard

@Deprecated
void discard()
             throws ContradictionException

Deprecated.

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.

Throws:

ContradictionException - if a trivial inconsistency is detected.

See Also:

discardCurrentSolution()

discardCurrentSolution

void discardCurrentSolution()
                            throws ContradictionException

Discard the current solution in the optimization problem.

Throws:

ContradictionException - if a trivial inconsistency is detected.

Since:

2.1

isOptimal

boolean isOptimal()

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

Returns:

setTimeoutForFindingBetterSolution

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

Since:

2.3.3