org.sat4j.pb.tools

Class SteppedTimeoutLexicoDecoratorPB

java.lang.Object

org.sat4j.tools.SolverDecorator<T>

org.sat4j.tools.LexicoDecorator<IPBSolver>

org.sat4j.pb.tools.LexicoDecoratorPB

org.sat4j.pb.tools.SteppedTimeoutLexicoDecoratorPB

All Implemented Interfaces:

Serializable, IPBSolver, IOptimizationProblem, IProblem, ISolver, RandomAccessModel

public class SteppedTimeoutLexicoDecoratorPB
extends LexicoDecoratorPB

See Also:

Serialized Form

Field Summary

Fields inherited from class org.sat4j.pb.tools.LexicoDecoratorPB

objs

Fields inherited from class org.sat4j.tools.LexicoDecorator

criteria, currentCriterion, isSolutionOptimal, prevboolmodel, prevConstr, prevfullmodel, prevmodelwithinternalvars

Constructor Summary

Constructors

Constructor and Description
SteppedTimeoutLexicoDecoratorPB(IPBSolver solver)

Method Summary

Methods

Modifier and Type	Method and Description
boolean	admitABetterSolution(IVecInt assumps) Look for a solution of the optimization problem when some literals are satisfied.

Methods inherited from class org.sat4j.pb.tools.LexicoDecoratorPB

addAtLeast, addAtLeast, addAtMost, addAtMost, addCriterion, addCriterion, addExactly, addExactly, addPseudoBoolean, discardSolutionsForOptimizing, evaluate, evaluate, fixCriterionValue, getObjectiveFunction, numberOfCriteria, setObjectiveFunction

Methods inherited from class org.sat4j.tools.LexicoDecorator

admitABetterSolution, calculateObjective, discard, discardCurrentSolution, forceObjectiveValueTo, getObjectiveValue, getObjectiveValue, hasNoObjectiveFunction, isOptimal, manageUnsatCase, model, model, modelWithInternalVariables, nonOptimalMeansSatisfiable, setTimeoutForFindingBetterSolution

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

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

Methods inherited from interface org.sat4j.specs.IProblem

findModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, nConstraints, newVar, nVars, primeImplicant, primeImplicant, printInfos, printInfos

Methods inherited from interface org.sat4j.specs.RandomAccessModel

model

Constructor Detail

SteppedTimeoutLexicoDecoratorPB

public SteppedTimeoutLexicoDecoratorPB(IPBSolver solver)

Method Detail

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 LexicoDecoratorPB

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)