org.sat4j.pb

Class PseudoOptDecorator

java.lang.Object

org.sat4j.tools.SolverDecorator<IPBSolver>

org.sat4j.pb.PBSolverDecorator

org.sat4j.pb.PseudoOptDecorator

All Implemented Interfaces:

Serializable, IPBSolver, IOptimizationProblem, IProblem, ISolver, RandomAccessModel

Direct Known Subclasses:

PseudoIteratorDecorator

public class PseudoOptDecorator
extends PBSolverDecorator
implements IOptimizationProblem

A decorator that computes minimal pseudo boolean models.

Author:

daniel

See Also:

Serialized Form

Constructor Summary

Constructors

Constructor and Description
PseudoOptDecorator(IPBSolver solver) Create a PB decorator for which a non optimal solution means that the problem is satisfiable.
PseudoOptDecorator(IPBSolver solver, boolean nonOptimalMeansSatisfiable) Create a PB decorator with a specific semantic of non optimal solution.
PseudoOptDecorator(IPBSolver solver, boolean nonOptimalMeansSatisfiable, boolean useAnImplicantForEvaluation) Create a PB decorator with a specific semantic of non optimal solution.

Method Summary

Methods

Modifier and Type	Method and Description
boolean	admitABetterSolution()
boolean	admitABetterSolution(IVecInt assumps)
Number	calculateObjective()
void	discard()
void	discardCurrentSolution()
void	forceObjectiveValueTo(Number forcedValue)
Number	getObjectiveValue()
boolean	hasNoObjectiveFunction()
boolean	isOptimal()
boolean	isSatisfiable()
boolean	isSatisfiable(boolean global)
boolean	isSatisfiable(IVecInt assumps)
boolean	isSatisfiable(IVecInt assumps, boolean global)
int[]	model()
boolean	model(int var)
int[]	modelWithInternalVariables()
boolean	nonOptimalMeansSatisfiable()
void	reset()
void	setObjectiveFunction(ObjectiveFunction objf) Provide an objective function to the solver.
void	setTimeout(int t)
void	setTimeoutForFindingBetterSolution(int seconds)
String	toString(String prefix)

Methods inherited from class org.sat4j.pb.PBSolverDecorator

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

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, isSolverKeptHot, isVerbose, nConstraints, newVar, newVar, nextFreeVarId, nVars, primeImplicant, primeImplicant, printInfos, printInfos, printStat, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeoutMs, setTimeoutOnConflicts, setUnitClauseProvider, 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, nConstraints, newVar, nVars, primeImplicant, primeImplicant, printInfos, printInfos

Methods inherited from interface org.sat4j.specs.ISolver

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

Constructor Detail

PseudoOptDecorator

public PseudoOptDecorator(IPBSolver solver)

Create a PB decorator for which a non optimal solution means that the problem is satisfiable.

Parameters:

solver - a PB solver.

PseudoOptDecorator

public PseudoOptDecorator(IPBSolver solver,
                  boolean nonOptimalMeansSatisfiable)

Create a PB decorator with a specific semantic of non optimal solution.

Parameters:

solver - a PB solver

nonOptimalMeansSatisfiable - true if a suboptimal solution means that the problem is satisfiable (e.g. as in the PB competition), else false (e.g. as in the MAXSAT competition).

PseudoOptDecorator

public PseudoOptDecorator(IPBSolver solver,
                  boolean nonOptimalMeansSatisfiable,
                  boolean useAnImplicantForEvaluation)

Create a PB decorator with a specific semantic of non optimal solution.

Parameters:

solver - a PB solver

nonOptimalMeansSatisfiable - true if a suboptimal solution means that the problem is satisfiable (e.g. as in the PB competition), else false (e.g. as in the MAXSAT competition).

useAnImplicantForEvaluation - uses an implicant (a prime implicant computed using SolverDecorator.primeImplicant()) instead of a plain model to evaluate the objective function.

Method Detail

isSatisfiable

public boolean isSatisfiable()
                      throws TimeoutException

Specified by:

isSatisfiable in interface IProblem

Overrides:

isSatisfiable in class SolverDecorator<IPBSolver>

Throws:

TimeoutException

isSatisfiable

public boolean isSatisfiable(boolean global)
                      throws TimeoutException

Specified by:

isSatisfiable in interface IProblem

Overrides:

isSatisfiable in class SolverDecorator<IPBSolver>

Throws:

TimeoutException

isSatisfiable

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

Specified by:

isSatisfiable in interface IProblem

Overrides:

isSatisfiable in class SolverDecorator<IPBSolver>

Throws:

TimeoutException

isSatisfiable

public boolean isSatisfiable(IVecInt assumps)
                      throws TimeoutException

Specified by:

isSatisfiable in interface IProblem

Overrides:

isSatisfiable in class SolverDecorator<IPBSolver>

Throws:

TimeoutException

setObjectiveFunction

public void setObjectiveFunction(ObjectiveFunction objf)

Description copied from interface: IPBSolver

Provide an objective function to the solver.

Specified by:

setObjectiveFunction in interface IPBSolver

Overrides:

setObjectiveFunction in class PBSolverDecorator

Parameters:

objf - the objective function

admitABetterSolution

public boolean admitABetterSolution()
                             throws TimeoutException

Specified by:

admitABetterSolution in interface IOptimizationProblem

Throws:

TimeoutException

admitABetterSolution

public boolean admitABetterSolution(IVecInt assumps)
                             throws TimeoutException

Specified by:

admitABetterSolution in interface IOptimizationProblem

Throws:

TimeoutException

hasNoObjectiveFunction

public boolean hasNoObjectiveFunction()

Specified by:

hasNoObjectiveFunction in interface IOptimizationProblem

nonOptimalMeansSatisfiable

public boolean nonOptimalMeansSatisfiable()

Specified by:

nonOptimalMeansSatisfiable in interface IOptimizationProblem

calculateObjective

public Number calculateObjective()

Specified by:

calculateObjective in interface IOptimizationProblem

discardCurrentSolution

public void discardCurrentSolution()
                            throws ContradictionException

Specified by:

discardCurrentSolution in interface IOptimizationProblem

Throws:

ContradictionException

reset

public void reset()

Specified by:

reset in interface ISolver

Overrides:

reset in class SolverDecorator<IPBSolver>

model

public int[] model()

Specified by:

model in interface IProblem

Overrides:

model in class SolverDecorator<IPBSolver>

model

public boolean model(int var)

Specified by:

model in interface RandomAccessModel

Overrides:

model in class SolverDecorator<IPBSolver>

toString

public String toString(String prefix)

Specified by:

toString in interface ISolver

Overrides:

toString in class SolverDecorator<IPBSolver>

getObjectiveValue

public Number getObjectiveValue()

Specified by:

getObjectiveValue in interface IOptimizationProblem

discard

public void discard()
             throws ContradictionException

Specified by:

discard in interface IOptimizationProblem

Throws:

ContradictionException

forceObjectiveValueTo

public void forceObjectiveValueTo(Number forcedValue)
                           throws ContradictionException

Specified by:

forceObjectiveValueTo in interface IOptimizationProblem

Throws:

ContradictionException

isOptimal

public boolean isOptimal()

Specified by:

isOptimal in interface IOptimizationProblem

modelWithInternalVariables

public int[] modelWithInternalVariables()

Specified by:

modelWithInternalVariables in interface ISolver

Overrides:

modelWithInternalVariables in class SolverDecorator<IPBSolver>

setTimeoutForFindingBetterSolution

public void setTimeoutForFindingBetterSolution(int seconds)

Specified by:

setTimeoutForFindingBetterSolution in interface IOptimizationProblem

setTimeout

public void setTimeout(int t)

Specified by:

setTimeout in interface ISolver

Overrides:

setTimeout in class SolverDecorator<IPBSolver>