org.sat4j.pb.tools
Class XplainPB

java.lang.Object
  org.sat4j.tools.SolverDecorator<T>
      org.sat4j.tools.xplain.Xplain<IPBSolver>
          org.sat4j.pb.tools.XplainPB

All Implemented Interfaces:

Serializable, IPBSolver, IProblem, ISolver

public class XplainPB
extends Xplain<IPBSolver>
implements IPBSolver

See Also:

Serialized Form

Field Summary

Fields inherited from class org.sat4j.tools.xplain.Xplain

assump, constrs

Constructor Summary

XplainPB(IPBSolver solver)

Method Summary

IConstr	addAtLeast(IVecInt literals, int degree)
IConstr	addAtMost(IVecInt literals, int degree)
IConstr	addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d) Create a Pseudo-Boolean constraint of the type "at least n of those literals must be satisfied"
ObjectiveFunction	getObjectiveFunction()
void	setObjectiveFunction(ObjectiveFunction obj)

Methods inherited from class org.sat4j.tools.xplain.Xplain

addClause, cancelExplanation, createNewVar, discardLastestVar, explain, findModel, findModel, getConstraints, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model

Methods inherited from class org.sat4j.tools.SolverDecorator

addAllClauses, addBlockingClause, clearDecorated, clearLearntClauses, decorated, expireTimeout, getLogPrefix, getSearchListener, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isVerbose, model, nConstraints, newVar, newVar, nextFreeVarId, nVars, printInfos, printStat, printStat, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, toString, 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.ISolver

addAllClauses, addBlockingClause, addClause, clearLearntClauses, expireTimeout, getLogPrefix, getSearchListener, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isVerbose, newVar, newVar, nextFreeVarId, printStat, printStat, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, toString, unsatExplanation

Methods inherited from interface org.sat4j.specs.IProblem

findModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, model, nConstraints, nVars, printInfos

Constructor Detail

XplainPB

public XplainPB(IPBSolver solver)

Method Detail

addAtLeast

public IConstr addAtLeast(IVecInt literals,
                          int degree)
                   throws ContradictionException

Specified by:

addAtLeast in interface ISolver

Overrides:

addAtLeast in class Xplain<IPBSolver>

Throws:

ContradictionException

addAtMost

public IConstr addAtMost(IVecInt literals,
                         int degree)
                  throws ContradictionException

Specified by:

addAtMost in interface ISolver

Overrides:

addAtMost in class Xplain<IPBSolver>

Throws:

ContradictionException

addPseudoBoolean

public IConstr addPseudoBoolean(IVecInt lits,
                                IVec<BigInteger> coeffs,
                                boolean moreThan,
                                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)

setObjectiveFunction

public void setObjectiveFunction(ObjectiveFunction obj)

Specified by:

setObjectiveFunction in interface IPBSolver

getObjectiveFunction

public ObjectiveFunction getObjectiveFunction()

Specified by:

getObjectiveFunction in interface IPBSolver