public class PBSolverResCP extends PBSolverCP
Modifier and Type | Field and Description |
---|---|
static long |
MAXCONFLICTS |
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 |
---|
PBSolverResCP(LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf,
IOrder order) |
PBSolverResCP(LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf,
IOrder order,
long bound) |
PBSolverResCP(LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf,
SearchParams params,
IOrder order) |
PBSolverResCP(LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf,
SearchParams params,
IOrder order,
RestartStrategy restarter) |
Modifier and Type | Method and Description |
---|---|
void |
claBumpActivity(Constr arg0) |
analyze, analyzeCP, toString, updateNumberOfReducedLearnedConstraints, updateNumberOfReductions
addAtLeast, addAtLeast, addAtMost, addAtMost, addAtMostOnTheFly, addAtMostOnTheFly, addExactly, addExactly, addPseudoBoolean, 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 static final long MAXCONFLICTS
public PBSolverResCP(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order)
public PBSolverResCP(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order, long bound)
public PBSolverResCP(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, SearchParams params, IOrder order, RestartStrategy restarter)
public PBSolverResCP(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, SearchParams params, IOrder order)
public void claBumpActivity(Constr arg0)
Copyright © 2013 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.