org.sat4j.specs
Interface IOptimizationProblem

All Superinterfaces:

IProblem

All Known Implementing Classes:

AbstractSelectorVariablesDecorator, ConstraintRelaxingPseudoOptDecorator, LexicoDecorator, LexicoDecoratorPB, MaxSatDecorator, MinCostDecorator, MinOneDecorator, PseudoIteratorDecorator, PseudoOptDecorator

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