org.sat4j.pb
Interface IPBSolver

All Superinterfaces:
IProblem, ISolver, java.io.Serializable
All Known Implementing Classes:
OPBStringSolver, OptToPBSATAdapter, PBSolver, PBSolverClause, PBSolverCP, PBSolverDecorator, PBSolverMerging, PBSolverResolution, PBSolverWithImpliedClause, PseudoOptDecorator

public interface IPBSolver
extends ISolver

A solver able to deal with pseudo boolean constraints.

Author:
daniel

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 listOfVariables)
           
 void setObjectiveFunction(ObjectiveFunction obj)
           
 
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
 

Method Detail

addPseudoBoolean

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

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

void setListOfVariablesForExplanation(IVecInt listOfVariables)

getExplanation

java.lang.String getExplanation()

setObjectiveFunction

void setObjectiveFunction(ObjectiveFunction obj)


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