|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object org.sat4j.tools.SolverDecorator<T> org.sat4j.tools.xplain.Xplain<IPBSolver> org.sat4j.pb.tools.XplainPB
public class XplainPB
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)
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. |
Methods inherited from class org.sat4j.tools.xplain.Xplain |
---|
addClause, cancelExplanation, createNewVar, discardLastestVar, explain, findModel, findModel, getConstraints, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, minimalExplanation, model, removeConstr, removeSubsumedConstr, setMinimizationStrategy, toString |
Methods inherited from class java.lang.Object |
---|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait |
Methods inherited from interface org.sat4j.specs.IProblem |
---|
findModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, model, nConstraints, newVar, nVars, primeImplicant, printInfos |
Constructor Detail |
---|
public XplainPB(IPBSolver solver)
Method Detail |
---|
public IConstr addAtLeast(IVecInt literals, int degree) throws ContradictionException
ISolver
addAtLeast
in interface ISolver
addAtLeast
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 constraint
ContradictionException
- 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
ISolver
addAtMost
in interface ISolver
addAtMost
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 constraint
ContradictionException
- 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
ISolver
addExactly
in interface ISolver
addExactly
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 satisfied
ContradictionException
- iff the constraint is trivially unsatisfiable.public IConstr addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d) throws ContradictionException
IPBSolver
addPseudoBoolean
in interface IPBSolver
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, false if it is a
constraint <= degreed
- the degree of the cardinality constraint
ContradictionException
- iff the vector of literals is empty or if the constraint is
falsified after unit propagationISolver.removeConstr(IConstr)
public void setObjectiveFunction(ObjectiveFunction obj)
IPBSolver
setObjectiveFunction
in interface IPBSolver
obj
- the objective functionpublic ObjectiveFunction getObjectiveFunction()
IPBSolver
getObjectiveFunction
in interface IPBSolver
public IConstr addAtMost(IVecInt literals, IVecInt coeffs, int degree) throws ContradictionException
IPBSolver
addAtMost
in interface IPBSolver
literals
- 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 constraint
ContradictionException
- iff the constraint is found trivially unsat.ISolver.removeConstr(IConstr)
public IConstr addAtMost(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree) throws ContradictionException
IPBSolver
addAtMost
in interface IPBSolver
literals
- 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 constraint
ContradictionException
- iff the constraint is found trivially unsat.ISolver.removeConstr(IConstr)
public IConstr addAtLeast(IVecInt literals, IVecInt coeffs, int degree) throws ContradictionException
IPBSolver
addAtLeast
in interface IPBSolver
literals
- 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 constraint
ContradictionException
- iff the constraint is found trivially unsat.ISolver.removeConstr(IConstr)
public IConstr addAtLeast(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree) throws ContradictionException
IPBSolver
addAtLeast
in interface IPBSolver
literals
- 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 constraint
ContradictionException
- iff the constraint is found trivially unsat.ISolver.removeConstr(IConstr)
public IConstr addExactly(IVecInt literals, IVecInt coeffs, int weight) throws ContradictionException
IPBSolver
addExactly
in interface IPBSolver
literals
- 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 satisfied
ContradictionException
- iff the constraint is trivially unsatisfiable.public IConstr addExactly(IVecInt literals, IVec<BigInteger> coeffs, BigInteger weight) throws ContradictionException
IPBSolver
addExactly
in interface IPBSolver
literals
- 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 satisfied
ContradictionException
- iff the constraint is trivially unsatisfiable.
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |