org.sat4j.opt
Class MinOneDecorator

java.lang.Object
  extended by org.sat4j.tools.SolverDecorator
      extended by 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.

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, decorated, getStat, getTimeout, isSatisfiable, isSatisfiable, model, nConstraints, newVar, newVar, nVars, printStat, printStat, removeConstr, setExpectedNumberOfClauses, setTimeout, toString
 
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 
Methods inherited from interface org.sat4j.specs.IProblem
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() 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.

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