org.sat4j.pb.core
Class PBSolverCP

java.lang.Object
  org.sat4j.minisat.core.Solver<PBDataStructureFactory>
      org.sat4j.pb.core.PBSolver
          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

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)
void	analyzeCP(Constr myconfl, Pair results)
String	toString(String prefix)
protected void	updateNumberOfReducedLearnedConstraints(IConflict confl)
protected void	updateNumberOfReductions(IConflict confl)

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, analyzeFinalConflictInTermsOfAssumptions, assume, cancelUntil, claBumpActivity, clearLearntClauses, decayActivities, decisionLevel, dimacs2internal, enqueue, enqueue, expireTimeout, findModel, findModel, getDSFactory, getIthConstr, getLogPrefix, getOrder, getOutLearnt, getSearchListener, getStat, getStats, getTimeout, getTimeoutMs, getVocabulary, initStats, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, isVerbose, learn, model, model, nAssigns, nConstraints, newVar, newVar, nextFreeVarId, nVars, printInfos, printLearntClausesInfos, printStat, printStat, propagate, reduceDB, 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, clearLearntClauses, expireTimeout, getLogPrefix, getSearchListener, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isVerbose, newVar, newVar, nextFreeVarId, printStat, printStat, 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, 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>

analyzeCP

public void analyzeCP(Constr myconfl,
                      Pair results)

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)