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:
java.io.Serializable, Learner, UnitPropagationListener, IPBSolver, IProblem, ISolver
Direct Known Subclasses:
PBSolverClause, PBSolverMerging, 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.minisat.core.Solver
analyzer, dsfactory, EXPENSIVE_SIMPLIFICATION, GLUCOSE, MEMORY_BASED, NO_SIMPLIFICATION, rootLevel, SIMPLE_SIMPLIFICATION, trail, trailLim, voc
 
Constructor Summary
PBSolverCP(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order)
           
PBSolverCP(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, SearchParams params, IOrder order)
           
PBSolverCP(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, SearchParams params, IOrder order, RestartStrategy restarter)
           
 
Method Summary
 void analyze(Constr myconfl, Pair results)
           
 java.lang.String toString(java.lang.String prefix)
           
 
Methods inherited from class org.sat4j.pb.core.PBSolver
addPseudoBoolean, getObjectiveFunction, setObjectiveFunction
 
Methods inherited from class org.sat4j.minisat.core.Solver
addAllClauses, addAtLeast, addAtMost, addBlockingClause, addClause, addConstr, analyzeAtRootLevel, assume, cancelUntil, claBumpActivity, clearLearntClauses, decayActivities, decisionLevel, dimacs2internal, enqueue, enqueue, expireTimeout, findModel, findModel, getDSFactory, getIthConstr, getOrder, getOutLearnt, getStat, getStats, getTimeout, getTimeoutMs, getVocabulary, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, learn, model, model, nAssigns, nConstraints, newVar, newVar, nextFreeVarId, nVars, printInfos, printLearntClausesInfos, printStat, printStat, propagate, reduceDB, removeConstr, removeSubsumedConstr, reset, setDataStructureFactory, setDBSimplificationAllowed, setExpectedNumberOfClauses, setLearnedConstraintsDeletionStrategy, setOrder, setRestartStrategy, setSearchListener, setSearchParams, setSimplifier, setSimplifier, setTimeout, setTimeoutMs, setTimeoutOnConflicts, simplifyDB, toString, undoOne, 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, clearLearntClauses, expireTimeout, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, newVar, newVar, nextFreeVarId, printStat, printStat, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts
 
Methods inherited from interface org.sat4j.specs.IProblem
findModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, model, nConstraints, nVars, printInfos
 

Constructor Detail

PBSolverCP

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

PBSolverCP

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

PBSolverCP

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

analyze

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

toString

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


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