org.sat4j.opt

Class MinOneDecorator

java.lang.Object

org.sat4j.tools.SolverDecorator<ISolver>

org.sat4j.opt.MinOneDecorator

All Implemented Interfaces:

Serializable, IOptimizationProblem, IProblem, ISolver, RandomAccessModel

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

Constructors

Constructor and Description
MinOneDecorator(ISolver solver)

Method Summary

Methods

Modifier and Type	Method and Description
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.
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.
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.
void	reset() Clean up the internal state of the solver.
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, model, nConstraints, newVar, newVar, nextFreeVarId, nVars, primeImplicant, primeImplicant, printInfos, printInfos, printStat, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, 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

Methods inherited from interface org.sat4j.specs.RandomAccessModel

model

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)

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

reset

public void reset()

Description copied from interface: ISolver

Clean up the internal state of the solver. Note that such method should also be called when you no longer need the solver because the state of the solver may prevent the GC to proceed. There is a known issue for instance where failing to call reset() on a solver will keep timer threads alive and exhausts memory.

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

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