org.sat4j.tools
Class LexicoDecorator<T extends ISolver>

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

public class LexicoDecorator<T extends ISolver>
extends SolverDecorator<T>
implements IOptimizationProblem

See Also:
Serialized Form

Field Summary
protected  List<IVecInt> criteria
           
protected  int currentCriterion
           
protected  boolean[] prevboolmodel
           
protected  int[] prevfullmodel
           
 
Constructor Summary
LexicoDecorator(T solver)
           
 
Method Summary
 void addCriterion(IVecInt literals)
           
 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.
protected  IConstr discardSolutionsForOptimizing()
           
protected  Number evaluate()
           
protected  void fixCriterionValue()
           
 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.
 boolean isOptimal()
          Allows to check afterwards if the solution provided by the solver is optimal or not.
 int[] model()
          Provide a model (if any) for a satisfiable formula.
 boolean model(int var)
          Provide the truth value of a specific variable in the model.
 boolean nonOptimalMeansSatisfiable()
          A suboptimal solution has different meaning depending of the optimization problem considered.
protected  int numberOfCriteria()
           
 
Methods inherited from class org.sat4j.tools.SolverDecorator
addAllClauses, addAtLeast, addAtMost, addBlockingClause, addClause, addExactly, clearDecorated, clearLearntClauses, decorated, expireTimeout, findModel, findModel, getLogPrefix, getSearchListener, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, isSolverKeptHot, isVerbose, modelWithInternalVariables, nConstraints, newVar, newVar, nextFreeVarId, nVars, primeImplicant, primeImplicant, printInfos, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, 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, nConstraints, newVar, nVars, primeImplicant, primeImplicant, printInfos
 

Field Detail

criteria

protected final List<IVecInt> criteria

currentCriterion

protected int currentCriterion

prevfullmodel

protected int[] prevfullmodel

prevboolmodel

protected boolean[] prevboolmodel
Constructor Detail

LexicoDecorator

public LexicoDecorator(T solver)
Method Detail

addCriterion

public void addCriterion(IVecInt literals)

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.
See Also:
ISolver.setTimeout(int)

numberOfCriteria

protected int numberOfCriteria()

fixCriterionValue

protected void fixCriterionValue()
                          throws ContradictionException
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<T extends ISolver>
Returns:
a model of the formula as an array of literals to satisfy.
See Also:
IProblem.isSatisfiable(), IProblem.isSatisfiable(IVecInt)

model

public boolean model(int var)
Description copied from interface: IProblem
Provide the truth value of a specific variable in the model. 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<T extends ISolver>
Parameters:
var - the variable id in Dimacs format
Returns:
the truth value of that variable in the model
See Also:
IProblem.model()

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()

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.

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

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()

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.

discardSolutionsForOptimizing

protected IConstr discardSolutionsForOptimizing()
                                         throws ContradictionException
Throws:
ContradictionException

evaluate

protected Number evaluate()

isOptimal

public boolean isOptimal()
Description copied from interface: IOptimizationProblem
Allows to check afterwards if the solution provided by the solver is optimal or not.

Specified by:
isOptimal in interface IOptimizationProblem
Returns:


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