org.sat4j.opt
Class MinOneDecorator

java.lang.Object
  org.sat4j.tools.SolverDecorator<ISolver>
      org.sat4j.opt.MinOneDecorator

All Implemented Interfaces:

java.io.Serializable, IOptimizationProblem, IProblem, ISolver

public class MinOneDecorator
extends SolverDecorator<ISolver>
implements IOptimizationProblem

Computes a solution with the smallest number of satisfied literals. Please make sure that newVar(howmany) is called first to setup the decorator.

Author:

leberre

See Also:

Serialized Form

Constructor Summary

MinOneDecorator(ISolver solver)

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.
int[]	model() Provide a model (if any) for a satisfiable formula.
boolean	nonOptimalMeansSatisfiable() A suboptimal solution has different meaning depending of the optimization problem considered.
void	reset() Clean up the internal state of the solver.

Methods inherited from class org.sat4j.tools.SolverDecorator

addAllClauses, addAtLeast, addAtMost, addClause, clearDecorated, clearLearntClauses, decorated, expireTimeout, findModel, findModel, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, nConstraints, newVar, newVar, nVars, printInfos, printStat, printStat, removeConstr, setDBSimplificationAllowed, setExpectedNumberOfClauses, setTimeout, setTimeoutMs, setTimeoutOnConflicts, toString

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface org.sat4j.specs.IProblem

findModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, nConstraints, nVars, printInfos

Constructor Detail

MinOneDecorator

public MinOneDecorator(ISolver solver)

Method Detail

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)

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 java.lang.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.

Specified by:

calculateObjective in interface IOptimizationProblem

Returns:

the value of the objective function.

discard

public void discard()
             throws ContradictionException

Description copied from interface: IOptimizationProblem

Discard the current solution in the optimization problem.

Specified by:

discard in interface IOptimizationProblem

Throws:

ContradictionException - if a trivial inconsistency is detected.

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<ISolver>

Returns:

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

See Also:

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

reset

public void reset()

Description copied from interface: ISolver

Clean up the internal state of the solver.

Specified by:

reset in interface ISolver

Overrides:

reset in class SolverDecorator<ISolver>