org.sat4j.minisat.constraints.pb
Class PBSolver<L extends ILits>

java.lang.Object
  org.sat4j.minisat.core.Solver<L>
      org.sat4j.minisat.constraints.pb.PBSolver<L>

All Implemented Interfaces:

java.io.Serializable, Learner, UnitPropagationListener, IProblem, ISolver

Direct Known Subclasses:

PBSolverClause, PBSolverMerging, PBSolverWithImpliedClause

public class PBSolver<L extends ILits>
extends Solver<L>

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, NO_SIMPLIFICATION, rootLevel, SIMPLE_SIMPLIFICATION, trail, trailLim, voc

Constructor Summary

PBSolver(AssertingClauseGenerator acg, LearningStrategy<L> learner, DataStructureFactory<L> dsf, IOrder<L> order)

PBSolver(AssertingClauseGenerator acg, LearningStrategy<L> learner, DataStructureFactory<L> dsf, SearchParams params, IOrder<L> order)

PBSolver(AssertingClauseGenerator acg, LearningStrategy<L> learner, DataStructureFactory<L> dsf, SearchParams params, IOrder<L> order, RestartStrategy restarter)

Method Summary

int	analyze(Constr myconfl, Handle<Constr> outLearntRef)
java.lang.String	toString(java.lang.String prefix) Display a textual representation of the solver configuration.

Methods inherited from class org.sat4j.minisat.core.Solver

addAllClauses, addAtLeast, addAtMost, addClause, addConstr, addPseudoBoolean, assume, cancelUntil, claBumpActivity, clearLearntClauses, decayActivities, decisionLevel, decode2dimacs, dimacs2internal, enqueue, enqueue, findModel, findModel, getDSFactory, getIthConstr, getOrder, getOutLearnt, getStat, getStats, getTimeout, getVocabulary, isSatisfiable, isSatisfiable, learn, model, model, nAssigns, nConstraints, newVar, newVar, nVars, printStat, printStat, propagate, reduceDB, reduceDB, removeConstr, reset, setDataStructureFactory, setExpectedNumberOfClauses, setOrder, setRestartStrategy, setSearchListener, setSearchParams, setSimplifier, setSimplifier, setTimeout, setTimeoutMs, simplifyDB, toString, undoOne, varBumpActivity

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Constructor Detail

PBSolver

public PBSolver(AssertingClauseGenerator acg,
                LearningStrategy<L> learner,
                DataStructureFactory<L> dsf,
                IOrder<L> order)

Parameters:

acg -

learner -

dsf -

PBSolver

public PBSolver(AssertingClauseGenerator acg,
                LearningStrategy<L> learner,
                DataStructureFactory<L> dsf,
                SearchParams params,
                IOrder<L> order,
                RestartStrategy restarter)

PBSolver

public PBSolver(AssertingClauseGenerator acg,
                LearningStrategy<L> learner,
                DataStructureFactory<L> dsf,
                SearchParams params,
                IOrder<L> order)

Method Detail

analyze

public int analyze(Constr myconfl,
                   Handle<Constr> outLearntRef)

Overrides:

analyze in class Solver<L extends ILits>

toString

public java.lang.String toString(java.lang.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<L extends ILits>

Parameters:

prefix - the prefix to use on each line.

Returns:

a textual description of the solver internals.