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:
- Serializable, Constr, Propagatable, Undoable, IWatchPb, PBConstr, IConstr
public final class PuebloMinWatchPb
- extends MinWatchPb
- See Also:
- Serialized Form
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 |
normalizedMinWatchPbNew
public static PuebloMinWatchPb normalizedMinWatchPbNew(UnitPropagationListener s,
ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree)
throws ContradictionException
- Parameters:
s
- a unit propagation listenervoc
- the vocabularylits
- the literalscoefs
- the coefficientsdegree
- 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 literalspIndice
- 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.