org.sat4j.pb.core
Class PBSolverCautious

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

All Implemented Interfaces:

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

public class PBSolverCautious
extends PBSolverCP

See Also:

Serialized Form

Field Summary

static int

BOUND

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

PBSolverCautious(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order)

PBSolverCautious(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order, int bound)

Method Summary

void	claBumpActivity(Constr confl)
String	toString(String prefix) Display a textual representation of the solver configuration.
protected void	updateNumberOfReducedLearnedConstraints(IConflict confl)
protected void	updateNumberOfReductions(IConflict confl)

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

analyze, analyzeCP

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

BOUND

public static final int BOUND

See Also:

Constant Field Values

Constructor Detail

PBSolverCautious

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

PBSolverCautious

public PBSolverCautious(LearningStrategy<PBDataStructureFactory> learner,
                        PBDataStructureFactory dsf,
                        IOrder order,
                        int bound)

Method Detail

toString

public String toString(String prefix)

Description copied from interface: ISolver

Display a textual representation of the solver configuration.

Specified by:

toString in interface ISolver

Overrides:

toString in class PBSolverCP

Parameters:

prefix - the prefix to use on each line.

Returns:

a textual description of the solver internals.

updateNumberOfReductions

protected void updateNumberOfReductions(IConflict confl)

Overrides:

updateNumberOfReductions in class PBSolverCP

updateNumberOfReducedLearnedConstraints

protected void updateNumberOfReducedLearnedConstraints(IConflict confl)

Overrides:

updateNumberOfReducedLearnedConstraints in class PBSolverCP

claBumpActivity

public void claBumpActivity(Constr confl)

Parameters:

outclause -