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, Learner, UnitPropagationListener, IPBSolver, IProblem, ISolver
Direct Known Subclasses:
PBSolverCautious, PBSolverClause, PBSolverMerging, 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
stats
 
Fields inherited from class org.sat4j.minisat.core.Solver
dsfactory, EXPENSIVE_SIMPLIFICATION, EXPENSIVE_SIMPLIFICATION_WLONLY, glucose, memory_based, NO_SIMPLIFICATION, rootLevel, SIMPLE_SIMPLIFICATION, 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)
           
 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.PBSolver
addAtLeast, addAtLeast, addAtMost, addAtMost, addExactly, addExactly, addPseudoBoolean, getObjectiveFunction, setObjectiveFunction
 
Methods inherited from class org.sat4j.minisat.core.Solver
addAllClauses, addAtLeast, addAtMost, addBlockingClause, addClause, addConstr, addExactly, analyzeAtRootLevel, analyzeFinalConflictInTermsOfAssumptions, assume, cancelUntil, claBumpActivity, clearLearntClauses, decayActivities, decisionLevel, dimacs2internal, enqueue, enqueue, expireTimeout, findModel, findModel, fixedSize, getDSFactory, getIthConstr, getLogPrefix, getOrder, getOutLearnt, getSearchListener, getStat, getStats, getTimeout, getTimeoutMs, getVocabulary, initStats, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, isVerbose, learn, model, model, modelWithInternalVariables, nAssigns, nConstraints, newVar, newVar, nextFreeVarId, nVars, primeImplicant, printInfos, printLearntClausesInfos, printStat, printStat, propagate, realNumberOfVariables, reduceDB, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDataStructureFactory, setDBSimplificationAllowed, setExpectedNumberOfClauses, setLearnedConstraintsDeletionStrategy, setLearner, setLogPrefix, setOrder, setRestartStrategy, setSearchListener, setSearchParams, setSimplifier, setSimplifier, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, simplifyDB, toString, 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.specs.ISolver
addAllClauses, addAtLeast, addAtMost, addBlockingClause, addClause, addExactly, clearLearntClauses, expireTimeout, getLogPrefix, getSearchListener, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isVerbose, modelWithInternalVariables, newVar, nextFreeVarId, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, 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, printInfos
 

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 - if the timeout is reached during conflict analysis.

analyzeCP

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

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 Solver<PBDataStructureFactory>
Parameters:
prefix - the prefix to use on each line.
Returns:
a textual description of the solver internals.

updateNumberOfReductions

protected void updateNumberOfReductions(IConflict confl)

updateNumberOfReducedLearnedConstraints

protected void updateNumberOfReducedLearnedConstraints(IConflict confl)


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