org.sat4j.pb.core
Class PBSolverMerging

java.lang.Object
  org.sat4j.minisat.core.Solver<PBDataStructureFactory>
      org.sat4j.pb.core.PBSolver
          org.sat4j.pb.core.PBSolverCP
              org.sat4j.pb.core.PBSolverMerging

All Implemented Interfaces:

Serializable, Learner, UnitPropagationListener, IPBSolver, IProblem, ISolver

public class PBSolverMerging
extends PBSolverCP

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

PBSolverMerging(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order)

Method Summary

String

toString(String prefix) Display a textual representation of the solver configuration.

Methods inherited from class org.sat4j.pb.core.PBSolverCP

analyze, analyzeCP, updateNumberOfReducedLearnedConstraints, updateNumberOfReductions

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

PBSolverMerging

public PBSolverMerging(LearningStrategy<PBDataStructureFactory> learner,
                       PBDataStructureFactory dsf,
                       IOrder order)

Method Detail

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 PBSolverCP

Parameters:

prefix - the prefix to use on each line.

Returns:

a textual description of the solver internals.