org.sat4j.pb
Class PBSolverDecorator

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

public class PBSolverDecorator
extends SolverDecorator<IPBSolver>
implements IPBSolver

A decorator for the PB solvers.

Author:
daniel
See Also:
Serialized Form

Constructor Summary
PBSolverDecorator(IPBSolver solver)
           
 
Method Summary
 IConstr addPseudoBoolean(IVecInt lits, IVec<java.math.BigInteger> coeffs, boolean moreThan, java.math.BigInteger d)
          Create a Pseudo-Boolean constraint of the type "at least n of those literals must be satisfied"
 java.lang.String getExplanation()
           
 void setListOfVariablesForExplanation(IVecInt varExplain)
           
 void setObjectiveFunction(ObjectiveFunction obj)
           
 
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, model, model, nConstraints, newVar, newVar, nVars, printInfos, printStat, printStat, removeConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setTimeout, setTimeoutMs, setTimeoutOnConflicts, toString
 
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, toString
 
Methods inherited from interface org.sat4j.specs.IProblem
findModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, model, nConstraints, nVars, printInfos
 

Constructor Detail

PBSolverDecorator

public PBSolverDecorator(IPBSolver solver)
Method Detail

addPseudoBoolean

public IConstr addPseudoBoolean(IVecInt lits,
                                IVec<java.math.BigInteger> coeffs,
                                boolean moreThan,
                                java.math.BigInteger d)
                         throws ContradictionException
Description copied from interface: IPBSolver
Create a Pseudo-Boolean constraint of the type "at least n of those literals must be satisfied"

Specified by:
addPseudoBoolean in interface IPBSolver
Parameters:
lits - a set of literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.
coeffs - the coefficients of the literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.
moreThan - true if it is a constraint >= degree
d - the degree of the cardinality constraint
Returns:
a reference to the constraint added in the solver, to use in removeConstr().
Throws:
ContradictionException - iff the vector of literals is empty or if the constraint is falsified after unit propagation
See Also:
ISolver.removeConstr(IConstr)

setListOfVariablesForExplanation

public void setListOfVariablesForExplanation(IVecInt varExplain)
Specified by:
setListOfVariablesForExplanation in interface IPBSolver

getExplanation

public java.lang.String getExplanation()
Specified by:
getExplanation in interface IPBSolver

setObjectiveFunction

public void setObjectiveFunction(ObjectiveFunction obj)
Specified by:
setObjectiveFunction in interface IPBSolver


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