org.sat4j.tools

Class LexicoDecorator<T extends ISolver>

java.lang.Object

org.sat4j.tools.SolverDecorator<T>

org.sat4j.tools.LexicoDecorator<T>

All Implemented Interfaces:

Serializable, IOptimizationProblem, IProblem, ISolver, RandomAccessModel

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

See Also:

Serialized Form

Field Summary

Fields

Modifier and Type	Field and Description
protected List<IVecInt>	criteria
protected int	currentCriterion
protected boolean	isSolutionOptimal
protected boolean[]	prevboolmodel
protected IConstr	prevConstr
protected int[]	prevfullmodel
protected int[]	prevmodelwithinternalvars

Constructor Summary

Constructors

Constructor and Description
LexicoDecorator(T solver)

Method Summary

Methods

Modifier and Type	Method and Description
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 Number	evaluate(int criterion)
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.
Number	getObjectiveValue(int criterion)
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.
protected boolean	manageUnsatCase()
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.
int[]	modelWithInternalVariables() That method is designed to be used to retrieve the real model of the current set of constraints, i.e. to provide the truth value of boolean variables used internally in the solver (for encoding purposes for instance).
boolean	nonOptimalMeansSatisfiable() A suboptimal solution has different meaning depending of the optimization problem considered.
int	numberOfCriteria()
void	setTimeoutForFindingBetterSolution(int seconds) Allow to set a specific timeout when the solver is in optimization mode.

Methods inherited from class org.sat4j.tools.SolverDecorator

addAllClauses, addAtLeast, addAtMost, addBlockingClause, addClause, addExactly, clearDecorated, clearLearntClauses, decorated, expireTimeout, findModel, findModel, getLogPrefix, getSearchListener, getSolvingEngine, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, isSolverKeptHot, isVerbose, nConstraints, newVar, newVar, nextFreeVarId, nVars, primeImplicant, primeImplicant, printInfos, printInfos, printStat, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setUnitClauseProvider, 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, printInfos

Field Detail

criteria

protected final List<IVecInt> criteria

currentCriterion

protected int currentCriterion

prevConstr

protected IConstr prevConstr

prevfullmodel

protected int[] prevfullmodel

prevmodelwithinternalvars

protected int[] prevmodelwithinternalvars

prevboolmodel

protected boolean[] prevboolmodel

isSolutionOptimal

protected boolean isSolutionOptimal

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)

manageUnsatCase

protected boolean manageUnsatCase()

numberOfCriteria

public 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: RandomAccessModel

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 RandomAccessModel

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:

#model()

modelWithInternalVariables

public int[] modelWithInternalVariables()

Description copied from interface: ISolver

That method is designed to be used to retrieve the real model of the current set of constraints, i.e. to provide the truth value of boolean variables used internally in the solver (for encoding purposes for instance). If no variables are added in the solver, then Arrays.equals(model(),modelWithInternalVariables()). In case new variables are added to the solver, then the number of models returned by that method is greater of equal to the number of models returned by model() when using a ModelIterator.

Specified by:

modelWithInternalVariables in interface ISolver

Overrides:

modelWithInternalVariables in class SolverDecorator<T extends ISolver>

Returns:

an array of literals, in Dimacs format, corresponding to a model of the formula over all the variables declared in the solver.

See Also:

IProblem.model(), ModelIterator

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.

getObjectiveValue

public Number getObjectiveValue(int criterion)

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

evaluate

protected Number evaluate(int criterion)

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:

setTimeoutForFindingBetterSolution

public void setTimeoutForFindingBetterSolution(int seconds)

Description copied from interface: IOptimizationProblem

Allow to set a specific timeout when the solver is in optimization mode. The solver internal timeout will be set to that value once it has found a solution. That way, the original timeout of the solver may be reduced if the solver finds quickly a solution, or increased if the solver finds regularly new solutions (thus giving more time to the solver each time).

Specified by:

setTimeoutForFindingBetterSolution in interface IOptimizationProblem