public class XplainPB extends Xplain<IPBSolver> implements IPBSolver
| Modifier and Type | Method and Description |
|---|---|
IConstr |
addAtLeast(IVecInt literals,
int degree)
Create a cardinality constraint of the type "at least n of those literals
must be satisfied"
|
IConstr |
addAtLeast(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree)
Create a pseudo-boolean constraint of the type "at least".
|
IConstr |
addAtLeast(IVecInt literals,
IVecInt coeffs,
int degree)
Create a pseudo-boolean constraint of the type "at least".
|
IConstr |
addAtMost(IVecInt literals,
int degree)
Create a cardinality constraint of the type "at most n of those literals
must be satisfied"
|
IConstr |
addAtMost(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger degree)
Create a pseudo boolean constraint of the type "at most".
|
IConstr |
addAtMost(IVecInt literals,
IVecInt coeffs,
int degree)
Create a pseudo boolean constraint of the type "at most".
|
IConstr |
addExactly(IVecInt literals,
int n)
Create a cardinality constraint of the type
"exactly n of those literals must be satisfied".
|
IConstr |
addExactly(IVecInt literals,
IVec<BigInteger> coeffs,
BigInteger weight)
Create a pseudo-boolean constraint of the type "subset sum".
|
IConstr |
addExactly(IVecInt literals,
IVecInt coeffs,
int weight)
Create a pseudo-boolean constraint of the type "subset sum".
|
IConstr |
addPseudoBoolean(IVecInt lits,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger d)
Create a Pseudo-Boolean constraint of the type "at least n or at most n
of those literals must be satisfied"
|
ObjectiveFunction |
getObjectiveFunction()
Retrieve the objective function from the solver.
|
void |
setObjectiveFunction(ObjectiveFunction obj)
Provide an objective function to the solver.
|
cancelExplanation, explain, findModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, minimalExplanation, removeConstr, removeSubsumedConstr, setMinimizationStrategy, toStringaddClause, addControlableClause, addNonControlableClause, getAddedVars, getConstraints, getConstrs, getLastClause, getLastConstr, isSkipDuplicatedEntries, model, setLastConstrcreateNewVar, discardLastestVar, externalState, internalStateaddAllClauses, addBlockingClause, clearDecorated, clearLearntClauses, decorated, expireTimeout, getLogPrefix, getSearchListener, getSolvingEngine, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSolverKeptHot, isVerbose, model, modelWithInternalVariables, nConstraints, newVar, newVar, nextFreeVarId, nVars, primeImplicant, primeImplicant, printInfos, printInfos, printStat, printStat, printStat, realNumberOfVariables, registerLiteral, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, toString, unsatExplanationclone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, waitaddAllClauses, addBlockingClause, addClause, clearLearntClauses, expireTimeout, getLogPrefix, getSearchListener, getSolvingEngine, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSolverKeptHot, isVerbose, modelWithInternalVariables, newVar, nextFreeVarId, printStat, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, toString, unsatExplanationfindModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, nConstraints, newVar, nVars, primeImplicant, primeImplicant, printInfos, printInfosmodelpublic XplainPB(IPBSolver solver)
public IConstr addAtLeast(IVecInt literals, int degree) throws ContradictionException
ISolveraddAtLeast in interface ISolveraddAtLeast in class Xplain<IPBSolver>literals - a set of literals. The vector can be reused since the solver
is not supposed to keep a reference to that vector.degree - the degree (n) of the cardinality constraintContradictionException - iff the vector of literals is empty or if degree literals are
not remaining unfalsified after unit propagationISolver.removeConstr(IConstr)public IConstr addAtMost(IVecInt literals, int degree) throws ContradictionException
ISolveraddAtMost in interface ISolveraddAtMost in class Xplain<IPBSolver>literals - a set of literals The vector can be reused since the solver is
not supposed to keep a reference to that vector.degree - the degree (n) of the cardinality constraintContradictionException - iff the vector of literals is empty or if it contains more
than degree satisfied literals after unit propagationISolver.removeConstr(IConstr)public IConstr addExactly(IVecInt literals, int n) throws ContradictionException
ISolveraddExactly in interface ISolveraddExactly in class Xplain<IPBSolver>literals - a set of literals. The vector can be reused since the solver
is not supposed to keep a reference to that vector.n - the number of literals that must be satisfiedContradictionException - iff the constraint is trivially unsatisfiable.public IConstr addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d) throws ContradictionException
IPBSolveraddPseudoBoolean in interface IPBSolverlits - 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, false if it is a
constraint <= degreed - the degree of the cardinality constraintContradictionException - iff the vector of literals is empty or if the constraint is
falsified after unit propagationISolver.removeConstr(IConstr)public void setObjectiveFunction(ObjectiveFunction obj)
IPBSolversetObjectiveFunction in interface IPBSolverobj - the objective functionpublic ObjectiveFunction getObjectiveFunction()
IPBSolvergetObjectiveFunction in interface IPBSolverpublic IConstr addAtMost(IVecInt literals, IVecInt coeffs, int degree) throws ContradictionException
IPBSolveraddAtMost in interface IPBSolverliterals - 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.degree - the degree of the pseudo-boolean constraintContradictionException - iff the constraint is found trivially unsat.ISolver.removeConstr(IConstr)public IConstr addAtMost(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree) throws ContradictionException
IPBSolveraddAtMost in interface IPBSolverliterals - 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.degree - the degree of the pseudo-boolean constraintContradictionException - iff the constraint is found trivially unsat.ISolver.removeConstr(IConstr)public IConstr addAtLeast(IVecInt literals, IVecInt coeffs, int degree) throws ContradictionException
IPBSolveraddAtLeast in interface IPBSolverliterals - 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.degree - the degree of the pseudo-boolean constraintContradictionException - iff the constraint is found trivially unsat.ISolver.removeConstr(IConstr)public IConstr addAtLeast(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree) throws ContradictionException
IPBSolveraddAtLeast in interface IPBSolverliterals - 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.degree - the degree of the pseudo-boolean constraintContradictionException - iff the constraint is found trivially unsat.ISolver.removeConstr(IConstr)public IConstr addExactly(IVecInt literals, IVecInt coeffs, int weight) throws ContradictionException
IPBSolveraddExactly in interface IPBSolverliterals - 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.weight - the number of literals that must be satisfiedContradictionException - iff the constraint is trivially unsatisfiable.public IConstr addExactly(IVecInt literals, IVec<BigInteger> coeffs, BigInteger weight) throws ContradictionException
IPBSolveraddExactly in interface IPBSolverliterals - 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.weight - the number of literals that must be satisfiedContradictionException - iff the constraint is trivially unsatisfiable.Copyright © 2013 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.