org.sat4j.pb.core
Class PBSolverCP

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
All Implemented Interfaces:
Serializable, ICDCL<PBDataStructureFactory>, Learner, UnitPropagationListener, IPBCDCLSolver<PBDataStructureFactory>, IPBSolver, IProblem, ISolver, ISolverService
Direct Known Subclasses:
PBSolverCautious, PBSolverClause, PBSolverResCP, PBSolverWithImpliedClause

public class PBSolverCP
extends PBSolver

Author:
parrain To change the template for this generated type comment go to Window - Preferences - Java - Code Generation - Code and Comments
See Also:
Serialized Form

Field Summary
 
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
PBSolverCP(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order)
           
PBSolverCP(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, SearchParams params, IOrder order)
           
PBSolverCP(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, SearchParams params, IOrder order, RestartStrategy restarter)
           
 
Method Summary
 void analyze(Constr myconfl, Pair results)
           
 void analyzeCP(Constr myconfl, Pair results)
           
 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.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
 

Constructor Detail

PBSolverCP

public PBSolverCP(LearningStrategy<PBDataStructureFactory> learner,
                  PBDataStructureFactory dsf,
                  IOrder order)
Parameters:
acg -
learner -
dsf -

PBSolverCP

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

PBSolverCP

public PBSolverCP(LearningStrategy<PBDataStructureFactory> learner,
                  PBDataStructureFactory dsf,
                  SearchParams params,
                  IOrder order)
Method Detail

analyze

public void analyze(Constr myconfl,
                    Pair results)
             throws TimeoutException
Overrides:
analyze in class Solver<PBDataStructureFactory>
Throws:
TimeoutException

analyzeCP

public void analyzeCP(Constr myconfl,
                      Pair results)
               throws TimeoutException
Throws:
TimeoutException

toString

public String toString(String prefix)
Specified by:
toString in interface ISolver
Overrides:
toString in class Solver<PBDataStructureFactory>

updateNumberOfReductions

protected void updateNumberOfReductions(IConflict confl)

updateNumberOfReducedLearnedConstraints

protected void updateNumberOfReducedLearnedConstraints(IConflict confl)

claBumpActivity

public void claBumpActivity(Constr arg0)


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