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:
java.io.Serializable, IPBSolver, IOptimizationProblem, IProblem, ISolver

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)
           
 
Method Summary
 boolean admitABetterSolution()
           
 java.lang.Number calculateObjective()
           
 void discard()
           
 boolean hasNoObjectiveFunction()
           
 int[] model()
           
 boolean model(int var)
           
 boolean nonOptimalMeansSatisfiable()
           
 void setObjectiveFunction(ObjectiveFunction objf)
           
 java.lang.String toString(java.lang.String prefix)
           
 
Methods inherited from class org.sat4j.pb.PBSolverDecorator
addPseudoBoolean, getExplanation, setListOfVariablesForExplanation
 
Methods inherited from class org.sat4j.tools.SolverDecorator
addAllClauses, addAtLeast, addAtMost, addClause, clearDecorated, clearLearntClauses, decorated, expireTimeout, findModel, findModel, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, nConstraints, newVar, newVar, nVars, printInfos, printStat, printStat, removeConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setTimeout, setTimeoutMs, setTimeoutOnConflicts
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 
Methods inherited from interface org.sat4j.specs.IProblem
findModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, nConstraints, nVars, printInfos
 
Methods inherited from interface org.sat4j.specs.ISolver
addAllClauses, addAtLeast, addAtMost, addClause, clearLearntClauses, expireTimeout, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, newVar, newVar, printStat, printStat, removeConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setTimeout, setTimeoutMs, setTimeoutOnConflicts
 

Constructor Detail

PseudoOptDecorator

public PseudoOptDecorator(IPBSolver solver)
Method Detail

setObjectiveFunction

public void setObjectiveFunction(ObjectiveFunction objf)
Specified by:
setObjectiveFunction in interface IPBSolver
Overrides:
setObjectiveFunction in class PBSolverDecorator

admitABetterSolution

public boolean admitABetterSolution()
                             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 java.lang.Number calculateObjective()
Specified by:
calculateObjective in interface IOptimizationProblem

discard

public void discard()
             throws ContradictionException
Specified by:
discard in interface IOptimizationProblem
Throws:
ContradictionException

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 java.lang.String toString(java.lang.String prefix)
Specified by:
toString in interface ISolver
Overrides:
toString in class SolverDecorator<IPBSolver>


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