|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object org.sat4j.tools.SolverDecorator<IPBSolver> org.sat4j.pb.PseudoBitsAdderDecorator
public class PseudoBitsAdderDecorator
A decorator that computes minimal pseudo boolean models.
Constructor Summary | |
---|---|
PseudoBitsAdderDecorator(IPBSolver solver)
|
Method Summary | |
---|---|
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,
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,
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. |
boolean |
isSatisfiable()
|
boolean |
isSatisfiable(IVecInt assumps)
|
static void |
main(String[] args)
|
void |
setObjectiveFunction(ObjectiveFunction objf)
Provide an objective function to the solver. |
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, model, model, nConstraints, newVar, nVars, primeImplicant, printInfos |
Constructor Detail |
---|
public PseudoBitsAdderDecorator(IPBSolver solver)
Method Detail |
---|
public void setObjectiveFunction(ObjectiveFunction objf)
IPBSolver
setObjectiveFunction
in interface IPBSolver
objf
- the objective functionpublic boolean isSatisfiable() throws TimeoutException
isSatisfiable
in interface IProblem
isSatisfiable
in class SolverDecorator<IPBSolver>
TimeoutException
public boolean isSatisfiable(IVecInt assumps) throws TimeoutException
isSatisfiable
in interface IProblem
isSatisfiable
in class SolverDecorator<IPBSolver>
TimeoutException
public static void main(String[] args)
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 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 |