org.sat4j.specs
Interface IOptimizationProblem

All Superinterfaces:

IProblem

All Known Implementing Classes:

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.calculateObjective());
                optproblem.discard();
            }
            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.
java.lang.Number	calculateObjective() Compute the value of the objective function for the current solution.
void	discard() Discard the current solution in the optimization problem.
boolean	hasNoObjectiveFunction() If the optimization problem has no objective function, then it is a simple decision problem.
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, nVars, 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)

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

java.lang.Number calculateObjective()

Compute the value of the objective function for the current solution. A call to that method only makes sense if hasNoObjectiveFunction()==false.

Returns:

the value of the objective function.

discard

void discard()
             throws ContradictionException

Discard the current solution in the optimization problem.

Throws:

ContradictionException - if a trivial inconsistency is detected.