org.sat4j.pb
Class OptToPBSATAdapter

java.lang.Object
  extended by org.sat4j.tools.SolverDecorator<IPBSolver>
      extended by org.sat4j.pb.PBSolverDecorator
          extended by org.sat4j.pb.OptToPBSATAdapter
All Implemented Interfaces:
java.io.Serializable, IPBSolver, IProblem, ISolver

public class OptToPBSATAdapter
extends PBSolverDecorator

Utility class to use optimization solvers instead of simple SAT solvers in code meant for SAT solvers.

Author:
daniel
See Also:
Serialized Form

Constructor Summary
OptToPBSATAdapter(IOptimizationProblem problem)
           
 
Method Summary
 boolean isSatisfiable()
           
 boolean isSatisfiable(boolean global)
           
 boolean isSatisfiable(IVecInt assumps)
           
 boolean isSatisfiable(IVecInt assumps, boolean global)
           
 int[] model()
           
 boolean model(int var)
           
 java.lang.String toString(java.lang.String prefix)
           
 
Methods inherited from class org.sat4j.pb.PBSolverDecorator
addPseudoBoolean, getExplanation, setListOfVariablesForExplanation, setObjectiveFunction
 
Methods inherited from class org.sat4j.tools.SolverDecorator
addAllClauses, addAtLeast, addAtMost, addClause, clearDecorated, clearLearntClauses, decorated, expireTimeout, findModel, findModel, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, 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.ISolver
addAllClauses, addAtLeast, addAtMost, addClause, clearLearntClauses, expireTimeout, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, newVar, newVar, printStat, printStat, removeConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setTimeout, setTimeoutMs, setTimeoutOnConflicts
 
Methods inherited from interface org.sat4j.specs.IProblem
findModel, findModel, nConstraints, nVars, printInfos
 

Constructor Detail

OptToPBSATAdapter

public OptToPBSATAdapter(IOptimizationProblem problem)
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

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.