org.sat4j.minisat.constraints.pb
Class MaxWatchPb

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

All Implemented Interfaces:

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

public class MaxWatchPb
extends WatchPb
implements java.io.Serializable

See Also:

Serialized Form

Field Summary

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

ATLEAST, ATMOST

Method Summary

static MaxWatchPb	maxWatchPbNew(UnitPropagationListener s, ILits voc, IVecInt ps, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
static MaxWatchPb	maxWatchPbNew(UnitPropagationListener s, ILits voc, IVecInt ps, IVecInt coefs, boolean moreThan, int degree)
static MaxWatchPb	normalizedMaxWatchPbNew(UnitPropagationListener s, ILits voc, ArrayPb mpb)
static MaxWatchPb	normalizedMaxWatchPbNew(UnitPropagationListener s, ILits voc, IDataStructurePB mpb)
boolean	propagate(UnitPropagationListener s, int p) Propagation de la valeur de v?
void	remove() Enl???
void	undo(int p) M?
static WatchPb	watchPbNew(ILits voc, IVecInt lits, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
static WatchPb	watchPbNew(ILits voc, IVecInt lits, IVecInt coefs, boolean moreThan, int degree)

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

assertConstraint, calcReason, coefficientsEqualToOne, computeAnImpliedClause, get, getActivity, getCoef, getCoefs, getDegree, getLits, getVocabulary, incActivity, isAssertive, learnt, locked, niceCheckedParameters, niceParameters, recalcLeftSide, recalcLeftSide, register, rescaleBy, setLearnt, simplify, size, slackConstraint, slackConstraint, toBigInt, toString, toVecBigInt

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

Method Detail

maxWatchPbNew

public static MaxWatchPb maxWatchPbNew(UnitPropagationListener s,
                                       ILits voc,
                                       IVecInt ps,
                                       IVecInt coefs,
                                       boolean moreThan,
                                       int degree)
                                throws ContradictionException

Parameters:

s - outil pour la propagation des litt?raux

ps - liste des litt?raux de la nouvelle contrainte

coefs - liste des coefficients des litt?raux de la contrainte

moreThan - d?termine si c'est une sup?rieure ou ?gal ? l'origine

degree - fournit le degr? de la contrainte

Returns:

une nouvelle clause si tout va bien, ou null si un conflit est d?tect?

Throws:

ContradictionException

maxWatchPbNew

public static MaxWatchPb maxWatchPbNew(UnitPropagationListener s,
                                       ILits voc,
                                       IVecInt ps,
                                       IVec<java.math.BigInteger> coefs,
                                       boolean moreThan,
                                       java.math.BigInteger degree)
                                throws ContradictionException

Parameters:

s - outil pour la propagation des litt?raux

ps - liste des litt?raux de la nouvelle contrainte

coefs - liste des coefficients des litt?raux de la contrainte

moreThan - d?termine si c'est une sup?rieure ou ?gal ? l'origine

degree - fournit le degr? de la contrainte

Returns:

une nouvelle clause si tout va bien, ou null si un conflit est d?tect?

Throws:

ContradictionException

normalizedMaxWatchPbNew

public static MaxWatchPb normalizedMaxWatchPbNew(UnitPropagationListener s,
                                                 ILits voc,
                                                 ArrayPb mpb)
                                          throws ContradictionException

Throws:

ContradictionException

propagate

public boolean propagate(UnitPropagationListener s,
                         int p)

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

Specified by:

propagate in interface Propagatable

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()

Enl???ve une contrainte du prouveur

Specified by:

remove in interface Constr

undo

public void undo(int p)

M?thode appel?e lors du backtrack

Specified by:

undo in interface Undoable

Parameters:

p - un litt?ral d?saffect?

watchPbNew

public static WatchPb watchPbNew(ILits voc,
                                 IVecInt lits,
                                 IVecInt coefs,
                                 boolean moreThan,
                                 int degree)

watchPbNew

public static WatchPb watchPbNew(ILits voc,
                                 IVecInt lits,
                                 IVec<java.math.BigInteger> coefs,
                                 boolean moreThan,
                                 java.math.BigInteger degree)

normalizedMaxWatchPbNew

public static MaxWatchPb normalizedMaxWatchPbNew(UnitPropagationListener s,
                                                 ILits voc,
                                                 IDataStructurePB mpb)
                                          throws ContradictionException

Parameters:

s - a unit propagation listener

voc - the vocabulary

mpb - the PB constraint to normalize.

Returns:

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

Throws:

ContradictionException