public abstract class PBSolver extends Solver<PBDataStructureFactory> implements IPBCDCLSolver<PBDataStructureFactory>, IPBSolverService
| Modifier and Type | Field and Description |
|---|---|
LearnedConstraintsDeletionStrategy |
objectiveFunctionBased |
protected PBSolverStats |
stats |
constrs, dsfactory, EXPENSIVE_SIMPLIFICATION, EXPENSIVE_SIMPLIFICATION_WLONLY, glucose, learnedConstraintsDeletionStrategy, learnts, memory_based, NO_SIMPLIFICATION, out, rootLevel, sharedConflict, SIMPLE_SIMPLIFICATION, slistener, trail, trailLim, undertimeout, voc| Constructor and Description |
|---|
PBSolver(LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf,
IOrder order,
RestartStrategy restarter) |
PBSolver(LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf,
SearchParams params,
IOrder order,
RestartStrategy restarter) |
| Modifier and Type | Method and Description |
|---|---|
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 |
addAtMostOnTheFly(IVecInt literals,
IVec<BigInteger> coefs,
BigInteger degree) |
IConstr |
addAtMostOnTheFly(IVecInt literals,
IVecInt coefs,
int degree) |
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 literals,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger degree)
Create a Pseudo-Boolean constraint of the type "at least n or at most n
of those literals must be satisfied"
|
void |
claBumpActivity(Constr arg0) |
ObjectiveFunction |
getObjectiveFunction()
Retrieve the objective function from the solver.
|
void |
setObjectiveFunction(ObjectiveFunction obj)
Provide an objective function to the solver.
|
addAllClauses, addAtLeast, addAtMost, addAtMostOnTheFly, addBlockingClause, addClause, addClauseOnTheFly, addConstr, addExactly, analyze, analyzeAtRootLevel, analyzeFinalConflictInTermsOfAssumptions, assume, backtrack, cancelUntil, claBumpActivity, clearLearntClauses, currentDecisionLevel, decayActivities, decisionLevel, dimacs2internal, enqueue, enqueue, expireTimeout, findModel, findModel, fixedSize, fromLastDecisionLevel, getDSFactory, getIthConstr, getLearnedConstraints, getLiteralsPropagatedAt, getLogger, getLogPrefix, getOrder, getOutLearnt, getRestartStrategy, getSearchListener, getSearchParams, getSimplifier, getSolvingEngine, getStat, getStats, getTimeout, getTimeoutMs, getVariableHeuristics, getVocabulary, initStats, isDBSimplificationAllowed, isNeedToReduceDB, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, isSolverKeptHot, isVerbose, learn, model, model, modelWithInternalVariables, nAssigns, nConstraints, newVar, newVar, nextFreeVarId, nVars, primeImplicant, primeImplicant, printInfos, printInfos, printLearntClausesInfos, printStat, printStat, printStat, propagate, realNumberOfVariables, reduceDB, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDataStructureFactory, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLearnedConstraintsDeletionStrategy, setLearnedConstraintsDeletionStrategy, setLearnedConstraintsDeletionStrategy, setLearner, setLearningStrategy, setLogger, setLogPrefix, setNeedToReduceDB, setOrder, setRestartStrategy, setSearchListener, setSearchParams, setSimplifier, setSimplifier, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setUnitClauseProvider, setVerbose, simplifyDB, sortOnActivity, stop, suggestNextLiteralToBranchOn, toString, toString, truthValue, undoOne, unsatExplanation, unset, varBumpActivityclone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, waitgetLogger, getOrder, getRestartStrategy, getSearchParams, getSimplifier, getStats, setDataStructureFactory, setLearnedConstraintsDeletionStrategy, setLearnedConstraintsDeletionStrategy, setLearnedConstraintsDeletionStrategy, setLearner, setLearningStrategy, setLogger, setNeedToReduceDB, setOrder, setRestartStrategy, setSearchParams, setSimplifier, setSimplifieraddAllClauses, addAtLeast, addAtMost, addBlockingClause, addClause, addExactly, 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, setUnitClauseProvider, setVerbose, toString, unsatExplanationfindModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, nConstraints, newVar, nVars, primeImplicant, primeImplicant, printInfos, printInfosmodelenqueue, enqueue, unsetvarBumpActivityaddAtMostOnTheFly, addClauseOnTheFly, backtrack, currentDecisionLevel, getLearnedConstraints, getLiteralsPropagatedAt, getLogPrefix, getVariableHeuristics, nVars, removeSubsumedConstr, stop, suggestNextLiteralToBranchOn, truthValueprotected PBSolverStats stats
public final LearnedConstraintsDeletionStrategy objectiveFunctionBased
public PBSolver(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order, RestartStrategy restarter)
public PBSolver(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, SearchParams params, IOrder order, RestartStrategy restarter)
public IConstr addPseudoBoolean(IVecInt literals, IVec<BigInteger> coeffs, boolean moreThan, BigInteger degree) throws ContradictionException
IPBSolveraddPseudoBoolean 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.moreThan - true if it is a constraint >= degree, false if it is a
constraint <= degreedegree - 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 IPBSolvergetObjectiveFunction in interface IPBSolverServicepublic 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.public IConstr addAtMostOnTheFly(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)
addAtMostOnTheFly in interface IPBSolverServicepublic IConstr addAtMostOnTheFly(IVecInt literals, IVecInt coefs, int degree)
addAtMostOnTheFly in interface IPBSolverServicepublic void claBumpActivity(Constr arg0)
Copyright © 2013 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.