org.sat4j.minisat.constraints.pb
Class PBSolverWithImpliedClause

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

All Implemented Interfaces:

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

public class PBSolverWithImpliedClause
extends PBSolver<ILits>

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

PBSolverWithImpliedClause(AssertingClauseGenerator acg, LearningStrategy<ILits> learner, DataStructureFactory<ILits> dsf, IOrder<ILits> order)

Method Summary

IConstr	addPseudoBoolean(IVecInt literals, IVec<java.math.BigInteger> coeffs, boolean moreThan, java.math.BigInteger degree) Create a Pseudo-Boolean constraint of the type "at least n of those literals must be satisfied"
java.lang.String	toString(java.lang.String prefix) Display a textual representation of the solver configuration.

Methods inherited from class org.sat4j.minisat.constraints.pb.PBSolver

analyze

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

addAllClauses, addAtLeast, addAtMost, addClause, addConstr, 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

PBSolverWithImpliedClause

public PBSolverWithImpliedClause(AssertingClauseGenerator acg,
                                 LearningStrategy<ILits> learner,
                                 DataStructureFactory<ILits> dsf,
                                 IOrder<ILits> order)

Method Detail

addPseudoBoolean

public IConstr addPseudoBoolean(IVecInt literals,
                                IVec<java.math.BigInteger> coeffs,
                                boolean moreThan,
                                java.math.BigInteger degree)
                         throws ContradictionException

Description copied from interface: ISolver

Create a Pseudo-Boolean constraint of the type "at least n of those literals must be satisfied"

Specified by:

addPseudoBoolean in interface ISolver

Overrides:

addPseudoBoolean in class Solver<ILits>

Parameters:

literals - a set of literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

coeffs - the coefficients of the literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

moreThan - true if it is a constraint >= degree

degree - the degree of the cardinality constraint

Returns:

a reference to the constraint added in the solver, to use in removeConstr().

Throws:

ContradictionException - iff the vector of literals is empty or if the constraint is falsified after unit propagation

See Also:

ISolver.removeConstr(IConstr)

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 PBSolver<ILits>

Parameters:

prefix - the prefix to use on each line.

Returns:

a textual description of the solver internals.