org.sat4j.pb.constraints.pb
Class PuebloMinWatchPb

java.lang.Object
  extended by org.sat4j.pb.constraints.pb.WatchPb
      extended by org.sat4j.pb.constraints.pb.MinWatchPb
          extended by org.sat4j.pb.constraints.pb.PuebloMinWatchPb
All Implemented Interfaces:
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
protected  BigInteger maximalCoefficient(int pIndice)
          the maximal coefficient for the watched literals
static PuebloMinWatchPb normalizedMinWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree)
           
static WatchPb normalizedWatchPbNew(ILits voc, IDataStructurePB mpb)
           
protected  BigInteger updateWatched(BigInteger mc, int pIndice)
          update arrays watched and watching w.r.t. the propagation of a literal.
 
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, calcReason, 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,
                                                       BigInteger[] coefs,
                                                       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 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 BigInteger updateWatched(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


Copyright © 2012 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.