org.sat4j.opt

Class MaxSatDecorator

java.lang.Object

org.sat4j.tools.SolverDecorator<ISolver>

org.sat4j.opt.AbstractSelectorVariablesDecorator

org.sat4j.opt.MaxSatDecorator

All Implemented Interfaces:

Serializable, IOptimizationProblem, IProblem, ISolver, RandomAccessModel

public final class MaxSatDecorator
extends AbstractSelectorVariablesDecorator

Computes a solution that satisfies the maximum of clauses.

Author:

daniel

See Also:

Serialized Form

Constructor Summary

Constructors

Constructor and Description
MaxSatDecorator(ISolver solver)
MaxSatDecorator(ISolver solver, boolean equivalence)

Method Summary

Methods

Modifier and Type	Method and Description
IConstr	addClause(IVecInt literals) Create a clause from a set of literals The literals are represented by non null integers such that opposite literals a represented by opposite values.
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	nonOptimalMeansSatisfiable() A suboptimal solution has different meaning depending of the optimization problem considered.
void	reset() Clean up the internal state of the solver.
void	setExpectedNumberOfClauses(int nb) To inform the solver of the expected number of clauses to read.
void	setTimeoutForFindingBetterSolution(int seconds) Allow to set a specific timeout when the solver is in optimization mode.

Methods inherited from class org.sat4j.opt.AbstractSelectorVariablesDecorator

admitABetterSolution, getExpectedNumberOfClauses, getNbexpectedclauses, getPrevboolmodel, getPrevfullmodel, getPrevmodel, isOptimal, isSolutionOptimal, model, model, setNbexpectedclauses, setPrevboolmodel, setPrevfullmodel, setPrevmodel, setSolutionOptimal

Methods inherited from class org.sat4j.tools.SolverDecorator

addAllClauses, addAtLeast, addAtMost, addBlockingClause, addExactly, clearDecorated, clearLearntClauses, decorated, expireTimeout, findModel, findModel, getLogPrefix, getSearchListener, getSolvingEngine, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, isSolverKeptHot, isVerbose, modelWithInternalVariables, nConstraints, newVar, newVar, nextFreeVarId, nVars, primeImplicant, primeImplicant, printInfos, printInfos, printStat, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, setDBSimplificationAllowed, 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

Constructor Detail

MaxSatDecorator

public MaxSatDecorator(ISolver solver)

MaxSatDecorator

public MaxSatDecorator(ISolver solver,
               boolean equivalence)

Method Detail

setExpectedNumberOfClauses

public void setExpectedNumberOfClauses(int nb)

Description copied from interface: ISolver

To inform the solver of the expected number of clauses to read. This is an optional method, that is called when the p cnf line is read in dimacs formatted input file. Note that this method is supposed to be called AFTER a call to newVar(int)

Specified by:

setExpectedNumberOfClauses in interface ISolver

Overrides:

setExpectedNumberOfClauses in class AbstractSelectorVariablesDecorator

Parameters:

nb - the expected number of clauses.

See Also:

IProblem.newVar(int)

addClause

public IConstr addClause(IVecInt literals)
                  throws ContradictionException

Description copied from interface: ISolver

Create a clause from a set of literals The literals are represented by non null integers such that opposite literals a represented by opposite values. (classical Dimacs way of representing literals).

Specified by:

addClause in interface ISolver

Overrides:

addClause in class SolverDecorator<ISolver>

Parameters:

literals - a set of literals

Returns:

a reference to the constraint added in the solver, to use in removeConstr().

Throws:

ContradictionException - iff the vector of literals is empty or if it contains only falsified literals after unit propagation

See Also:

ISolver.removeConstr(IConstr)

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>

hasNoObjectiveFunction

public boolean hasNoObjectiveFunction()

Description copied from interface: IOptimizationProblem

If the optimization problem has no objective function, then it is a simple decision problem.

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.

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!

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.

Throws:

ContradictionException - if a trivial inconsistency is detected.

Since:

2.1

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

Overrides:

admitABetterSolution in class AbstractSelectorVariablesDecorator

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)

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.

Throws:

ContradictionException - if a trivial inconsistency is detected.

See Also:

IOptimizationProblem.discardCurrentSolution()

getObjectiveValue

public Number getObjectiveValue()

Description copied from interface: IOptimizationProblem

Read only access to the value of the objective function for the current solution.

Returns:

the value of the objective function for the current solution.

Since:

2.1

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.

Throws:

ContradictionException

Since:

2.1

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