org.sat4j.pb
Class ConstraintRelaxingPseudoOptDecorator

java.lang.Object
  org.sat4j.tools.SolverDecorator<IPBSolver>
      org.sat4j.pb.PBSolverDecorator
          org.sat4j.pb.ConstraintRelaxingPseudoOptDecorator

All Implemented Interfaces:

Serializable, IPBSolver, IOptimizationProblem, IProblem, ISolver

public class ConstraintRelaxingPseudoOptDecorator
extends PBSolverDecorator
implements IOptimizationProblem

Author:

lonca

See Also:

Serialized Form

Constructor Summary

ConstraintRelaxingPseudoOptDecorator(IPBSolver 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() Deprecated.
void	discard() Deprecated.
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.
boolean	isSatisfiable() Check the satisfiability of the set of constraints contained inside the solver.
boolean	isSatisfiable(boolean global) Check the satisfiability of the set of constraints contained inside the solver.
boolean	isSatisfiable(IVecInt assumps) Check the satisfiability of the set of constraints contained inside the solver.
boolean	isSatisfiable(IVecInt assumps, boolean global) Check the satisfiability of the set of constraints contained inside the solver.
boolean	nonOptimalMeansSatisfiable() A suboptimal solution has different meaning depending of the optimization problem considered.
String	toString(String prefix) Display a textual representation of the solver configuration.

Methods inherited from class org.sat4j.pb.PBSolverDecorator

addAtLeast, addAtLeast, addAtMost, addAtMost, addExactly, addExactly, addPseudoBoolean, getObjectiveFunction, setObjectiveFunction

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, isSolverKeptHot, isVerbose, model, model, 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, 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, model, model, nConstraints, newVar, nVars, primeImplicant, primeImplicant, printInfos

Methods inherited from interface org.sat4j.specs.ISolver

addAllClauses, addAtLeast, addAtMost, addBlockingClause, addClause, addExactly, clearLearntClauses, expireTimeout, getLogPrefix, getSearchListener, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSolverKeptHot, isVerbose, modelWithInternalVariables, newVar, nextFreeVarId, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, unsatExplanation

Constructor Detail

ConstraintRelaxingPseudoOptDecorator

public ConstraintRelaxingPseudoOptDecorator(IPBSolver solver)

Method Detail

isSatisfiable

public boolean isSatisfiable()
                      throws TimeoutException

Description copied from interface: IProblem

Check the satisfiability of the set of constraints contained inside the solver.

Specified by:

isSatisfiable in interface IProblem

Overrides:

isSatisfiable in class SolverDecorator<IPBSolver>

Returns:

true if the set of constraints is satisfiable, else false.

Throws:

TimeoutException

isSatisfiable

public boolean isSatisfiable(boolean global)
                      throws TimeoutException

Description copied from interface: IProblem

Check the satisfiability of the set of constraints contained inside the solver.

Specified by:

isSatisfiable in interface IProblem

Overrides:

isSatisfiable in class SolverDecorator<IPBSolver>

Parameters:

global - whether that call is part of a global process (i.e. optimization) or not. if (global), the timeout will not be reset between each call.

Returns:

true if the set of constraints is satisfiable, else false.

Throws:

TimeoutException

isSatisfiable

public boolean isSatisfiable(IVecInt assumps,
                             boolean global)
                      throws TimeoutException

Description copied from interface: IProblem

Check the satisfiability of the set of constraints contained inside the solver.

Specified by:

isSatisfiable in interface IProblem

Overrides:

isSatisfiable in class SolverDecorator<IPBSolver>

Parameters:

assumps - a set of literals (represented by usual non null integers in Dimacs format).

global - whether that call is part of a global process (i.e. optimization) or not. if (global), the timeout will not be reset between each call.

Returns:

true if the set of constraints is satisfiable when literals are satisfied, else false.

Throws:

TimeoutException

isSatisfiable

public boolean isSatisfiable(IVecInt assumps)
                      throws TimeoutException

Description copied from interface: IProblem

Check the satisfiability of the set of constraints contained inside the solver.

Specified by:

isSatisfiable in interface IProblem

Overrides:

isSatisfiable in class SolverDecorator<IPBSolver>

Parameters:

assumps - a set of literals (represented by usual non null integers in Dimacs format).

Returns:

true if the set of constraints is satisfiable when literals are satisfied, else false.

Throws:

TimeoutException

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)

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

@Deprecated
public Number calculateObjective()

Deprecated.

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

@Deprecated
public void discard()

Deprecated.

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

See Also:

IOptimizationProblem.discardCurrentSolution()

discardCurrentSolution

public void discardCurrentSolution()

Description copied from interface: IOptimizationProblem

Discard the current solution in the optimization problem.

Specified by:

discardCurrentSolution in interface IOptimizationProblem

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:

toString

public String toString(String prefix)

Description copied from interface: ISolver

Display a textual representation of the solver configuration.

Specified by:

toString in interface ISolver

Overrides:

toString in class SolverDecorator<IPBSolver>

Parameters:

prefix - the prefix to use on each line.

Returns:

a textual description of the solver internals.