public class PBSolverWithImpliedClause extends PBSolverCP
objectiveFunctionBased, 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 |
---|
PBSolverWithImpliedClause(LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf,
IOrder order) |
Modifier and Type | Method and Description |
---|---|
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) |
String |
toString(String prefix) |
analyze, analyzeCP, updateNumberOfReducedLearnedConstraints, updateNumberOfReductions
addAtLeast, addAtLeast, addAtMost, addAtMost, addAtMostOnTheFly, addAtMostOnTheFly, addExactly, addExactly, getObjectiveFunction, setObjectiveFunction
addAllClauses, addAtLeast, addAtMost, addAtMostOnTheFly, addBlockingClause, addClause, addClauseOnTheFly, addConstr, addExactly, analyzeAtRootLevel, analyzeFinalConflictInTermsOfAssumptions, assume, backtrack, cancelUntil, claBumpActivity, clearLearntClauses, currentDecisionLevel, decayActivities, decisionLevel, dimacs2internal, enqueue, enqueue, expireTimeout, findModel, findModel, fixedSize, 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, setVerbose, simplifyDB, sortOnActivity, stop, suggestNextLiteralToBranchOn, toString, truthValue, undoOne, unsatExplanation, unset, varBumpActivity
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getLogger, getOrder, getRestartStrategy, getSearchParams, getSimplifier, getStats, setDataStructureFactory, setLearnedConstraintsDeletionStrategy, setLearnedConstraintsDeletionStrategy, setLearnedConstraintsDeletionStrategy, setLearner, setLearningStrategy, setLogger, setNeedToReduceDB, setOrder, setRestartStrategy, setSearchParams, setSimplifier, setSimplifier
addAllClauses, 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, setVerbose, unsatExplanation
findModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, nConstraints, newVar, nVars, primeImplicant, primeImplicant, printInfos, printInfos
model
enqueue, enqueue, unset
varBumpActivity
addAtMostOnTheFly, addClauseOnTheFly, backtrack, currentDecisionLevel, getLearnedConstraints, getLiteralsPropagatedAt, getLogPrefix, getVariableHeuristics, nVars, removeSubsumedConstr, stop, suggestNextLiteralToBranchOn, truthValue
public PBSolverWithImpliedClause(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order)
public IConstr addPseudoBoolean(IVecInt literals, IVec<BigInteger> coeffs, boolean moreThan, BigInteger degree) throws ContradictionException
IPBSolver
addPseudoBoolean
in interface IPBSolver
addPseudoBoolean
in class PBSolver
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.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 String toString(String prefix)
toString
in interface ISolver
toString
in class PBSolverCP
public void claBumpActivity(Constr arg0)
Copyright © 2013 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.