org.sat4j.opt
Class MinOneDecorator

java.lang.Object
  extended by org.sat4j.tools.SolverDecorator<ISolver>
      extended by org.sat4j.opt.MinOneDecorator
All Implemented Interfaces:
Serializable, IOptimizationProblem, IProblem, ISolver

public final 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.
 boolean admitABetterSolution(IVecInt assumps)
          Look for a solution of the optimization problem when some literals are satisfied.
 Number calculateObjective()
          Compute the value of the objective function for the current solution.
 void discard()
          Discard the current solution in the optimization problem.
 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.
 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, addBlockingClause, addClause, clearDecorated, clearLearntClauses, decorated, expireTimeout, findModel, findModel, getLogPrefix, getSearchListener, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, isVerbose, model, nConstraints, newVar, newVar, nextFreeVarId, nVars, printInfos, printStat, printStat, removeConstr, removeSubsumedConstr, setDBSimplificationAllowed, setExpectedNumberOfClauses, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, toString, toString, unsatExplanation
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, 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)

admitABetterSolution

public boolean admitABetterSolution(IVecInt assumps)
                             throws TimeoutException
Description copied from interface: IOptimizationProblem
Look for a solution of the optimization problem when some literals are satisfied.

Specified by:
admitABetterSolution in interface IOptimizationProblem
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

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 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. DO NOT CALL THAT METHOD THAT WILL BE CALLED AUTOMATICALLY. USE getObjectiveValue() instead!

Specified by:
calculateObjective in interface IOptimizationProblem
Returns:
the value of the objective function.
See Also:
IOptimizationProblem.getObjectiveValue()

discardCurrentSolution

public void discardCurrentSolution()
                            throws ContradictionException
Description copied from interface: IOptimizationProblem
Discard the current solution in the optimization problem.

Specified by:
discardCurrentSolution in interface IOptimizationProblem
Throws:
ContradictionException - if a trivial inconsistency is detected.
Since:
2.1

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>

getObjectiveValue

public Number getObjectiveValue()
Description copied from interface: IOptimizationProblem
Read only access to the value of the objective function for the current solution.

Specified by:
getObjectiveValue in interface IOptimizationProblem
Returns:
the value of the objective function for the current solution.
Since:
2.1

discard

public void discard()
             throws ContradictionException
Description copied from interface: IOptimizationProblem
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.

Specified by:
discard in interface IOptimizationProblem
Throws:
ContradictionException - if a trivial inconsistency is detected.
See Also:
IOptimizationProblem.discardCurrentSolution()

forceObjectiveValueTo

public void forceObjectiveValueTo(Number forcedValue)
                           throws ContradictionException
Description copied from interface: IOptimizationProblem
Force the value of the objective function. This is especially useful to iterate over optimal solutions.

Specified by:
forceObjectiveValueTo in interface IOptimizationProblem
Throws:
ContradictionException
Since:
2.1


Copyright © 2010 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.