org.sat4j.pb
Class PseudoOptDecorator

java.lang.Object
  extended by org.sat4j.tools.SolverDecorator<IPBSolver>
      extended by org.sat4j.pb.PBSolverDecorator
          extended by org.sat4j.pb.PseudoOptDecorator
All Implemented Interfaces:
Serializable, IPBSolver, IOptimizationProblem, IProblem, ISolver
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
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
 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.
 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, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSolverKeptHot, isVerbose, nConstraints, newVar, newVar, nextFreeVarId, nVars, primeImplicant, primeImplicant, printInfos, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, 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, 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, newVar, nextFreeVarId, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, 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 IProblem
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>


Copyright © 2012 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.