org.sat4j.pb.constraints.pb

Class PuebloMinWatchPb

java.lang.Object

org.sat4j.pb.constraints.pb.WatchPb

org.sat4j.pb.constraints.pb.MinWatchPb

org.sat4j.pb.constraints.pb.PuebloMinWatchPb

All Implemented Interfaces:

java.io.Serializable, Constr, Propagatable, Undoable, IWatchPb, PBConstr, IConstr

public final class PuebloMinWatchPb
extends MinWatchPb

See Also:

Serialized Form

Field Summary

Fields inherited from class org.sat4j.pb.constraints.pb.MinWatchPb

watchCumul, watched, watching, watchingCount

Fields inherited from class org.sat4j.pb.constraints.pb.WatchPb

activity, coefs, degree, learnt, lits, sumcoefs, voc

Method Summary

Modifier and Type	Method and Description
protected java.math.BigInteger	maximalCoefficient(int pIndice) the maximal coefficient for the watched literals
static PuebloMinWatchPb	normalizedMinWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, java.math.BigInteger[] coefs, java.math.BigInteger degree)
static WatchPb	normalizedWatchPbNew(ILits voc, IDataStructurePB mpb)
protected java.math.BigInteger	updateWatched(java.math.BigInteger mc, int pIndice) update arrays watched and watching w.r.t.

Methods inherited from class org.sat4j.pb.constraints.pb.MinWatchPb

computePropagation, computeWatches, nbOfWatched, normalizedMinWatchPbNew, propagate, remove, undo

Methods inherited from class org.sat4j.pb.constraints.pb.WatchPb

assertConstraint, assertConstraintIfNeeded, calcReason, calcReasonOnTheFly, canBePropagatedMultipleTimes, coefficientsEqualToOne, computeAnImpliedClause, computeLeftSide, computeLeftSide, equals, forwardActivity, get, getActivity, getCoef, getCoefs, getDegree, getLits, getVocabulary, hashCode, incActivity, isAssertive, isSatisfiable, learnt, locked, ppcm, register, rescaleBy, setActivity, setLearnt, simplify, size, slackConstraint, slackConstraint, sort, sort, toConstraint, toString

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Method Detail

normalizedMinWatchPbNew

public static PuebloMinWatchPb normalizedMinWatchPbNew(UnitPropagationListener s,
                                                       ILits voc,
                                                       int[] lits,
                                                       java.math.BigInteger[] coefs,
                                                       java.math.BigInteger degree)
                                                throws ContradictionException

Parameters:

s - a unit propagation listener

voc - the vocabulary

lits - the literals

coefs - the coefficients

degree - the degree of the constraint to normalize.

Returns:

a new PB constraint or null if a trivial inconsistency is detected.

Throws:

ContradictionException

normalizedWatchPbNew

public static WatchPb normalizedWatchPbNew(ILits voc,
                                           IDataStructurePB mpb)

maximalCoefficient

protected java.math.BigInteger maximalCoefficient(int pIndice)

Description copied from class: MinWatchPb

the maximal coefficient for the watched literals

Overrides:

maximalCoefficient in class MinWatchPb

Parameters:

pIndice - propagated literal : its coefficient is excluded from the search of the maximal coefficient

Returns:

the maximal coefficient for the watched literals

updateWatched

protected java.math.BigInteger updateWatched(java.math.BigInteger mc,
                                             int pIndice)

Description copied from class: MinWatchPb

update arrays watched and watching w.r.t. the propagation of a literal. return the maximal coefficient of the watched literals (could have been changed).

Overrides:

updateWatched in class MinWatchPb

Parameters:

mc - the current maximal coefficient of the watched literals

pIndice - the literal propagated (falsified)

Returns:

the new maximal coefficient of the watched literals