org.sat4j.pb.core
Class PBSolverResCP

java.lang.Object
  org.sat4j.minisat.core.Solver<PBDataStructureFactory>
      org.sat4j.pb.core.PBSolver
          org.sat4j.pb.core.PBSolverCP
              org.sat4j.pb.core.PBSolverResCP

All Implemented Interfaces:

Serializable, ICDCL<PBDataStructureFactory>, Learner, UnitPropagationListener, IPBCDCLSolver<PBDataStructureFactory>, IPBSolver, IProblem, ISolver, ISolverService

public class PBSolverResCP
extends PBSolverCP

See Also:

Serialized Form

Field Summary

static long

MAXCONFLICTS

Fields inherited from class org.sat4j.pb.core.PBSolver

objectiveFunctionBased, stats

Fields inherited from class org.sat4j.minisat.core.Solver

constrs, dsfactory, EXPENSIVE_SIMPLIFICATION, EXPENSIVE_SIMPLIFICATION_WLONLY, glucose, learnedConstraintsDeletionStrategy, learnts, memory_based, NO_SIMPLIFICATION, out, rootLevel, SIMPLE_SIMPLIFICATION, slistener, trail, trailLim, undertimeout, voc

Constructor Summary

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)

Method Summary

void	claBumpActivity(Constr confl)

Methods inherited from class org.sat4j.pb.core.PBSolverCP

analyze, analyzeCP, toString, updateNumberOfReducedLearnedConstraints, updateNumberOfReductions

Methods inherited from class org.sat4j.pb.core.PBSolver

addAtLeast, addAtLeast, addAtMost, addAtMost, addExactly, addExactly, addPseudoBoolean, getObjectiveFunction, setObjectiveFunction

Methods inherited from class org.sat4j.minisat.core.Solver

addAllClauses, addAtLeast, addAtMost, addBlockingClause, addClause, addClause, 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, getSimplifier, 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, printLearntClausesInfos, printStat, printStat, propagate, realNumberOfVariables, reduceDB, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDataStructureFactory, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLearnedConstraintsDeletionStrategy, setLearnedConstraintsDeletionStrategy, setLearnedConstraintsDeletionStrategy, setLearner, setLogger, setLogPrefix, setNeedToReduceDB, setOrder, setRestartStrategy, setSearchListener, setSearchParams, setSimplifier, setSimplifier, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, simplifyDB, sortOnActivity, stop, suggestNextLiteralToBranchOn, toString, truthValue, undoOne, unsatExplanation, unset, varBumpActivity

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Methods inherited from interface org.sat4j.minisat.core.ICDCL

getLogger, getOrder, getRestartStrategy, getSimplifier, setDataStructureFactory, setLearnedConstraintsDeletionStrategy, setLearnedConstraintsDeletionStrategy, setLearnedConstraintsDeletionStrategy, setLearner, setLogger, setNeedToReduceDB, setOrder, setRestartStrategy, setSearchParams, setSimplifier, setSimplifier

Methods inherited from interface org.sat4j.specs.ISolver

addAllClauses, addAtLeast, addAtMost, addBlockingClause, addClause, addExactly, clearLearntClauses, expireTimeout, getLogPrefix, getSearchListener, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSolverKeptHot, isVerbose, modelWithInternalVariables, newVar, nextFreeVarId, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, unsatExplanation

Methods inherited from interface org.sat4j.specs.IProblem

findModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, model, nConstraints, newVar, nVars, primeImplicant, primeImplicant, printInfos

Methods inherited from interface org.sat4j.minisat.core.UnitPropagationListener

enqueue, enqueue, unset

Methods inherited from interface org.sat4j.minisat.core.VarActivityListener

varBumpActivity

Methods inherited from interface org.sat4j.minisat.core.Learner

learn

Field Detail

MAXCONFLICTS

public static final long MAXCONFLICTS

See Also:

Constant Field Values

Constructor Detail

PBSolverResCP

public PBSolverResCP(LearningStrategy<PBDataStructureFactory> learner,
                     PBDataStructureFactory dsf,
                     IOrder order)

PBSolverResCP

public PBSolverResCP(LearningStrategy<PBDataStructureFactory> learner,
                     PBDataStructureFactory dsf,
                     IOrder order,
                     long bound)

PBSolverResCP

public PBSolverResCP(LearningStrategy<PBDataStructureFactory> learner,
                     PBDataStructureFactory dsf,
                     SearchParams params,
                     IOrder order,
                     RestartStrategy restarter)

PBSolverResCP

public PBSolverResCP(LearningStrategy<PBDataStructureFactory> learner,
                     PBDataStructureFactory dsf,
                     SearchParams params,
                     IOrder order)

Method Detail

claBumpActivity

public void claBumpActivity(Constr confl)

Parameters:

outclause -