org.sat4j.specs
Interface IOptimizationProblem

All Superinterfaces:
IProblem
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
 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.
 
Methods inherited from interface org.sat4j.specs.IProblem
findModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, model, nConstraints, newVar, nVars, primeImplicant, primeImplicant, printInfos
 

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:


Copyright © 2012 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.