public class ObjectiveReducerPBSolverDecorator extends Object implements IPBSolver
Constructor and Description |
---|
ObjectiveReducerPBSolverDecorator(IPBSolver decorated) |
Modifier and Type | Method and Description |
---|---|
void |
addAllClauses(IVec<IVecInt> clauses) |
IConstr |
addAtLeast(IVecInt literals,
int degree) |
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) |
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 |
addBlockingClause(IVecInt literals) |
IConstr |
addClause(IVecInt literals) |
IConstr |
addExactly(IVecInt literals,
int n) |
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"
|
void |
clearLearntClauses() |
void |
expireTimeout() |
int[] |
findModel() |
int[] |
findModel(IVecInt assumps) |
String |
getLogPrefix() |
ObjectiveFunction |
getObjectiveFunction()
Retrieve the objective function from the solver.
|
<S extends ISolverService> |
getSearchListener() |
ISolver |
getSolvingEngine() |
Map<String,Number> |
getStat() |
int |
getTimeout() |
long |
getTimeoutMs() |
boolean |
isDBSimplificationAllowed() |
boolean |
isSatisfiable() |
boolean |
isSatisfiable(boolean globalTimeout) |
boolean |
isSatisfiable(IVecInt assumps) |
boolean |
isSatisfiable(IVecInt assumps,
boolean globalTimeout) |
boolean |
isSolverKeptHot() |
boolean |
isVerbose() |
int[] |
model() |
boolean |
model(int var) |
int[] |
modelWithInternalVariables() |
int |
nConstraints() |
int |
newVar() |
int |
newVar(int howmany) |
int |
nextFreeVarId(boolean reserve) |
int |
nVars() |
int[] |
primeImplicant() |
boolean |
primeImplicant(int p) |
void |
printInfos(PrintWriter out) |
void |
printInfos(PrintWriter out,
String prefix) |
void |
printStat(PrintStream out,
String prefix) |
void |
printStat(PrintWriter out) |
void |
printStat(PrintWriter out,
String prefix) |
int |
realNumberOfVariables() |
void |
registerLiteral(int p) |
boolean |
removeConstr(IConstr c) |
boolean |
removeSubsumedConstr(IConstr c) |
void |
reset() |
void |
setDBSimplificationAllowed(boolean status) |
void |
setExpectedNumberOfClauses(int nb) |
void |
setKeepSolverHot(boolean keepHot) |
void |
setLogPrefix(String prefix) |
void |
setObjectiveFunction(ObjectiveFunction obj)
Provide an objective function to the solver.
|
<S extends ISolverService> |
setSearchListener(SearchListener<S> sl) |
void |
setTimeout(int t) |
void |
setTimeoutMs(long t) |
void |
setTimeoutOnConflicts(int count) |
void |
setVerbose(boolean value) |
String |
toString(String prefix) |
IVecInt |
unsatExplanation() |
public ObjectiveReducerPBSolverDecorator(IPBSolver decorated)
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 constraintContradictionException
- iff the vector of literals is empty or if the constraint is
falsified after unit propagationISolver.removeConstr(IConstr)
public boolean model(int var)
model
in interface RandomAccessModel
public int nextFreeVarId(boolean reserve)
nextFreeVarId
in interface ISolver
public int[] primeImplicant()
primeImplicant
in interface IProblem
public boolean primeImplicant(int p)
primeImplicant
in interface IProblem
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 constraintContradictionException
- iff the constraint is found trivially unsat.ISolver.removeConstr(IConstr)
public boolean isSatisfiable() throws TimeoutException
isSatisfiable
in interface IProblem
TimeoutException
public boolean isSatisfiable(IVecInt assumps, boolean globalTimeout) throws TimeoutException
isSatisfiable
in interface IProblem
TimeoutException
public void registerLiteral(int p)
registerLiteral
in interface ISolver
public void setExpectedNumberOfClauses(int nb)
setExpectedNumberOfClauses
in interface ISolver
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 constraintContradictionException
- iff the constraint is found trivially unsat.ISolver.removeConstr(IConstr)
public boolean isSatisfiable(boolean globalTimeout) throws TimeoutException
isSatisfiable
in interface IProblem
TimeoutException
public IConstr addClause(IVecInt literals) throws ContradictionException
addClause
in interface ISolver
ContradictionException
public boolean isSatisfiable(IVecInt assumps) throws TimeoutException
isSatisfiable
in interface IProblem
TimeoutException
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 constraintContradictionException
- iff the constraint is found trivially unsat.ISolver.removeConstr(IConstr)
public int[] findModel() throws TimeoutException
findModel
in interface IProblem
TimeoutException
public IConstr addBlockingClause(IVecInt literals) throws ContradictionException
addBlockingClause
in interface ISolver
ContradictionException
public boolean removeConstr(IConstr c)
removeConstr
in interface ISolver
public int[] findModel(IVecInt assumps) throws TimeoutException
findModel
in interface IProblem
TimeoutException
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 constraintContradictionException
- iff the constraint is found trivially unsat.ISolver.removeConstr(IConstr)
public boolean removeSubsumedConstr(IConstr c)
removeSubsumedConstr
in interface ISolver
public int nConstraints()
nConstraints
in interface IProblem
public void addAllClauses(IVec<IVecInt> clauses) throws ContradictionException
addAllClauses
in interface ISolver
ContradictionException
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 satisfiedContradictionException
- iff the constraint is trivially unsatisfiable.public void printInfos(PrintWriter out, String prefix)
printInfos
in interface IProblem
public IConstr addAtMost(IVecInt literals, int degree) throws ContradictionException
addAtMost
in interface ISolver
ContradictionException
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 satisfiedContradictionException
- iff the constraint is trivially unsatisfiable.public void printInfos(PrintWriter out)
printInfos
in interface IProblem
public IConstr addAtLeast(IVecInt literals, int degree) throws ContradictionException
addAtLeast
in interface ISolver
ContradictionException
public void setObjectiveFunction(ObjectiveFunction obj)
IPBSolver
setObjectiveFunction
in interface IPBSolver
obj
- the objective functionpublic ObjectiveFunction getObjectiveFunction()
IPBSolver
getObjectiveFunction
in interface IPBSolver
public IConstr addExactly(IVecInt literals, int n) throws ContradictionException
addExactly
in interface ISolver
ContradictionException
public void setTimeout(int t)
setTimeout
in interface ISolver
public void setTimeoutOnConflicts(int count)
setTimeoutOnConflicts
in interface ISolver
public void setTimeoutMs(long t)
setTimeoutMs
in interface ISolver
public int getTimeout()
getTimeout
in interface ISolver
public long getTimeoutMs()
getTimeoutMs
in interface ISolver
public void expireTimeout()
expireTimeout
in interface ISolver
public void printStat(PrintStream out, String prefix)
public void printStat(PrintWriter out, String prefix)
public void printStat(PrintWriter out)
public void clearLearntClauses()
clearLearntClauses
in interface ISolver
public void setDBSimplificationAllowed(boolean status)
setDBSimplificationAllowed
in interface ISolver
public boolean isDBSimplificationAllowed()
isDBSimplificationAllowed
in interface ISolver
public <S extends ISolverService> void setSearchListener(SearchListener<S> sl)
setSearchListener
in interface ISolver
public <S extends ISolverService> SearchListener<S> getSearchListener()
getSearchListener
in interface ISolver
public void setVerbose(boolean value)
setVerbose
in interface ISolver
public void setLogPrefix(String prefix)
setLogPrefix
in interface ISolver
public String getLogPrefix()
getLogPrefix
in interface ISolver
public IVecInt unsatExplanation()
unsatExplanation
in interface ISolver
public int[] modelWithInternalVariables()
modelWithInternalVariables
in interface ISolver
public int realNumberOfVariables()
realNumberOfVariables
in interface ISolver
public boolean isSolverKeptHot()
isSolverKeptHot
in interface ISolver
public void setKeepSolverHot(boolean keepHot)
setKeepSolverHot
in interface ISolver
public ISolver getSolvingEngine()
getSolvingEngine
in interface ISolver
Copyright © 2013 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.