public class LPStringSolver extends DimacsStringSolver implements IPBSolver
firstConstr, fixedNbClauses, nbclauses, nbvars| Constructor and Description |
|---|
LPStringSolver() |
LPStringSolver(int initSize) |
| 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 |
addClause(IVecInt literals)
Create a clause from a set of literals The literals are represented by
non null integers such that opposite literals a represented by opposite
values.
|
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"
|
String |
getExplanation() |
ObjectiveFunction |
getObjectiveFunction()
Retrieve the objective function from the solver.
|
boolean |
isSatisfiable(IVecInt assumps)
Check the satisfiability of the set of constraints contained inside the
solver.
|
boolean |
isSatisfiable(IVecInt assumps,
boolean global)
Check the satisfiability of the set of constraints contained inside the
solver.
|
int |
nConstraints()
To know the number of constraints currently available in the solver.
|
int |
newVar(int howmany)
Declare
howmany variables in the problem (and thus in the
vocabulary), that will be represented using the Dimacs format by integers
ranging from 1 to howmany. |
void |
objectiveFunctionToLP(ObjectiveFunction obj,
StringBuffer buffer) |
void |
setExpectedNumberOfClauses(int nb)
To inform the solver of the expected number of clauses to read.
|
void |
setListOfVariablesForExplanation(IVecInt listOfVariables) |
void |
setObjectiveFunction(ObjectiveFunction obj)
Provide an objective function to the solver.
|
String |
toString() |
String |
toString(String prefix)
Display a textual representation of the solver configuration.
|
addExactly, getOut, modelWithInternalVariables, newVar, nextFreeVarId, nVars, primeImplicant, printInfos, printStat, realNumberOfVariables, registerLiteral, reset, setNbVarsaddAllClauses, addBlockingClause, clearLearntClauses, expireTimeout, findModel, findModel, getLogPrefix, getSearchListener, getSolvingEngine, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSolverKeptHot, isVerbose, model, model, primeImplicant, printInfos, printStat, printStat, removeConstr, removeSubsumedConstr, setDBSimplificationAllowed, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, unsatExplanationclone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, waitaddAllClauses, addBlockingClause, addExactly, clearLearntClauses, expireTimeout, getLogPrefix, getSearchListener, getSolvingEngine, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSolverKeptHot, isVerbose, modelWithInternalVariables, newVar, nextFreeVarId, printStat, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, unsatExplanationfindModel, findModel, isSatisfiable, isSatisfiable, model, nVars, primeImplicant, primeImplicant, printInfos, printInfosmodelpublic LPStringSolver()
public LPStringSolver(int initSize)
initSize - public boolean isSatisfiable(IVecInt assumps) throws TimeoutException
IProblemisSatisfiable in interface IProblemisSatisfiable in class AbstractOutputSolverassumps - a set of literals (represented by usual non null integers in
Dimacs format).TimeoutExceptionpublic boolean isSatisfiable(IVecInt assumps, boolean global) throws TimeoutException
IProblemisSatisfiable in interface IProblemisSatisfiable in class AbstractOutputSolverassumps - a set of literals (represented by usual non null integers in
Dimacs format).global - whether that call is part of a global process (i.e.
optimization) or not. if (global), the timeout will not be
reset between each call.TimeoutExceptionpublic 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 IConstr addAtLeast(IVecInt literals, int degree) throws ContradictionException
ISolveraddAtLeast in interface ISolveraddAtLeast in class DimacsStringSolverliterals - 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 DimacsStringSolverliterals - 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 addClause(IVecInt literals) throws ContradictionException
ISolveraddClause in interface ISolveraddClause in class DimacsStringSolverliterals - a set of literalsContradictionException - iff the vector of literals is empty or if it contains only
falsified literals after unit propagationISolver.removeConstr(IConstr)public String getExplanation()
public void setListOfVariablesForExplanation(IVecInt listOfVariables)
public void objectiveFunctionToLP(ObjectiveFunction obj, StringBuffer buffer)
public String toString()
toString in class DimacsStringSolverpublic String toString(String prefix)
ISolvertoString in interface ISolvertoString in class DimacsStringSolverprefix - the prefix to use on each line.public int newVar(int howmany)
IProblemhowmany variables in the problem (and thus in the
vocabulary), that will be represented using the Dimacs format by integers
ranging from 1 to howmany. That feature allows encodings to create
additional variables with identifier starting at howmany+1.newVar in interface IProblemnewVar in class DimacsStringSolverhowmany - number of variables to createIProblem.nVars()public void setExpectedNumberOfClauses(int nb)
ISolverp cnf line is
read in dimacs formatted input file.
Note that this method is supposed to be called AFTER a call to
newVar(int)setExpectedNumberOfClauses in interface ISolversetExpectedNumberOfClauses in class DimacsStringSolvernb - the expected number of clauses.IProblem.newVar(int)public ObjectiveFunction getObjectiveFunction()
IPBSolvergetObjectiveFunction in interface IPBSolverpublic int nConstraints()
IProblemnConstraints in interface IProblemnConstraints in class DimacsStringSolverpublic 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.