org.sat4j.opt
Class MinOneDecorator

java.lang.Object
  org.sat4j.tools.SolverDecorator
      org.sat4j.opt.MinOneDecorator

All Implemented Interfaces:

java.io.Serializable, IOptimizationProblem, IProblem, ISolver

public class MinOneDecorator
extends SolverDecorator
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()
java.lang.Number	calculateObjective()
void	discard()
boolean	hasNoObjectiveFunction()
int[]	model() Provide a model (if any) for a satisfiable formula.
boolean	nonOptimalMeansSatisfiable()
void	reset() Clean up the internal state of the solver.

Methods inherited from class org.sat4j.tools.SolverDecorator

addAllClauses, addAtLeast, addAtMost, addClause, addPseudoBoolean, clearLearntClauses, decorated, findModel, findModel, getStat, getTimeout, isSatisfiable, isSatisfiable, model, nConstraints, newVar, newVar, nVars, printStat, printStat, removeConstr, setExpectedNumberOfClauses, setTimeout, setTimeoutMs, 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, model, nConstraints, nVars

Constructor Detail

MinOneDecorator

public MinOneDecorator(ISolver solver)

Method Detail

admitABetterSolution

public boolean admitABetterSolution()
                             throws TimeoutException

Specified by:

admitABetterSolution in interface IOptimizationProblem

Throws:

TimeoutException

hasNoObjectiveFunction

public boolean hasNoObjectiveFunction()

Specified by:

hasNoObjectiveFunction in interface IOptimizationProblem

nonOptimalMeansSatisfiable

public boolean nonOptimalMeansSatisfiable()

Specified by:

nonOptimalMeansSatisfiable in interface IOptimizationProblem

calculateObjective

public java.lang.Number calculateObjective()

Specified by:

calculateObjective in interface IOptimizationProblem

discard

public void discard()
             throws ContradictionException

Specified by:

discard in interface IOptimizationProblem

Throws:

ContradictionException

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

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