org.sat4j.pb.constraints.pb
Class MaxWatchPb

java.lang.Object
  org.sat4j.pb.constraints.pb.WatchPb
      org.sat4j.pb.constraints.pb.MaxWatchPb

All Implemented Interfaces:

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

public class MaxWatchPb
extends WatchPb

See Also:

Serialized Form

Field Summary

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

activity, ATLEAST, ATMOST, coefs, degree, learnt, lits, voc, watchCumul

Method Summary

protected void	computePropagation(UnitPropagationListener s)
protected void	computeWatches() Permet l'observation de tous les litt???
static MaxWatchPb	normalizedMaxWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, java.math.BigInteger[] coefs, java.math.BigInteger degree)
static WatchPb	normalizedWatchPbNew(ILits voc, IDataStructurePB mpb)
boolean	propagate(UnitPropagationListener s, int p) Propagation de la valeur de v?
void	remove(UnitPropagationListener upl) Enl???
void	undo(int p) M?

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

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

Methods inherited from class java.lang.Object

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

Method Detail

computeWatches

protected void computeWatches()
                       throws ContradictionException

Permet l'observation de tous les litt???raux

Specified by:

computeWatches in class WatchPb

Throws:

ContradictionException

See Also:

WatchPb.computeWatches()

computePropagation

protected void computePropagation(UnitPropagationListener s)
                           throws ContradictionException

Specified by:

computePropagation in class WatchPb

Throws:

ContradictionException

propagate

public boolean propagate(UnitPropagationListener s,
                         int p)

Propagation de la valeur de v?rit? d'un litt?ral falsifi?

Parameters:

s - un prouveur

p - le litt?ral propag? (il doit etre falsifie)

Returns:

false ssi une inconsistance est d?tect?e

remove

public void remove(UnitPropagationListener upl)

Enl???ve une contrainte du prouveur

undo

public void undo(int p)

M?thode appel?e lors du backtrack

Parameters:

p - un litt?ral d?saffect?

normalizedMaxWatchPbNew

public static MaxWatchPb normalizedMaxWatchPbNew(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 of the constraint

coefs - the coefficients of the constraint

degree - the degree of the constraint

Returns:

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

Throws:

ContradictionException

normalizedWatchPbNew

public static WatchPb normalizedWatchPbNew(ILits voc,
                                           IDataStructurePB mpb)