org.sat4j.pb.core
Class PBSolverCautious

java.lang.Object
  extended by org.sat4j.minisat.core.Solver<PBDataStructureFactory>
      extended by org.sat4j.pb.core.PBSolver
          extended by org.sat4j.pb.core.PBSolverCP
              extended by 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 arg0)
           
 String toString(String prefix)
           
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)
Specified by:
toString in interface ISolver
Overrides:
toString in class PBSolverCP

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 arg0)


Copyright © 2012 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.