org.sat4j.pb.core
Class PBSolverResolution

java.lang.Object
  extended by org.sat4j.minisat.core.Solver<PBDataStructureFactory>
      extended by org.sat4j.pb.core.PBSolver
          extended by org.sat4j.pb.core.PBSolverResolution
All Implemented Interfaces:
java.io.Serializable, Learner, UnitPropagationListener, IPBSolver, IProblem, ISolver

public class PBSolverResolution
extends PBSolver

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
PBSolverResolution(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order, RestartStrategy restarter)
           
PBSolverResolution(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, SearchParams params, IOrder order, RestartStrategy restarter)
           
 
Method Summary
 
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, analyze, 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, 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, toString
 
Methods inherited from interface org.sat4j.specs.IProblem
findModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, model, nConstraints, nVars, printInfos
 

Constructor Detail

PBSolverResolution

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

PBSolverResolution

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


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