org.sat4j.minisat.constraints.pb
Class MinWatchPb

java.lang.Object
  extended by org.sat4j.minisat.constraints.pb.WatchPb
      extended by org.sat4j.minisat.constraints.pb.MinWatchPb
All Implemented Interfaces:
java.io.Serializable, PBConstr, Constr, Propagatable, Undoable, IConstr
Direct Known Subclasses:
PuebloMinWatchPb

public class MinWatchPb
extends WatchPb

See Also:
Serialized Form

Field Summary
protected  boolean[] watched
          Liste des indices des litt???
protected  int[] watching
          Sert ???
protected  int watchingCount
          Liste des indices des litt???
 
Fields inherited from class org.sat4j.minisat.constraints.pb.WatchPb
activity, ATLEAST, ATMOST, coefs, degree, learnt, lits, locked, voc, watchCumul
 
Constructor Summary
protected MinWatchPb(ILits voc, IDataStructurePB mpb)
          Constructeur de base des contraintes
protected MinWatchPb(ILits voc, int[] lits, java.math.BigInteger[] coefs, java.math.BigInteger degree)
           
 
Method Summary
protected  void computePropagation(UnitPropagationListener s)
           
protected  void computeWatches()
           
protected  java.math.BigInteger maximalCoefficient(int pIndice)
           
static MinWatchPb minWatchPbNew(UnitPropagationListener s, ILits voc, IVecInt ps, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
           
static MinWatchPb minWatchPbNew(UnitPropagationListener s, ILits voc, IVecInt ps, IVecInt coefs, boolean moreThan, int degree)
           
protected  int nbOfWatched()
          Nombre de litt???
static MinWatchPb normalizedMinWatchPbNew(UnitPropagationListener s, ILits voc, IDataStructurePB mpb)
           
static MinWatchPb normalizedMinWatchPbNew(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()
          Enl???
 void undo(int p)
          M???
protected  java.math.BigInteger updateWatched(java.math.BigInteger mc, int pIndice)
           
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, isSatisfiable, learnt, locked, niceCheckedParameters, niceParameters, ppcm, recalcLeftSide, recalcLeftSide, register, rescaleBy, setLearnt, simplify, size, slackConstraint, slackConstraint, sort, sort, toBigInt, toString, toVecBigInt
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Field Detail

watched

protected boolean[] watched
Liste des indices des litt???raux regardant la contrainte


watching

protected int[] watching
Sert ??? d???terminer si la clause est watched par le litt???ral


watchingCount

protected int watchingCount
Liste des indices des litt???raux regardant la contrainte

Constructor Detail

MinWatchPb

protected MinWatchPb(ILits voc,
                     IDataStructurePB mpb)
Constructeur de base des contraintes

Parameters:
voc - Informations sur le vocabulaire employ???
mpb - a mutable PB constraint

MinWatchPb

protected MinWatchPb(ILits voc,
                     int[] lits,
                     java.math.BigInteger[] coefs,
                     java.math.BigInteger degree)
Method Detail

computeWatches

protected void computeWatches()
                       throws ContradictionException
Specified by:
computeWatches in class WatchPb
Throws:
ContradictionException

computePropagation

protected void computePropagation(UnitPropagationListener s)
                           throws ContradictionException
Specified by:
computePropagation in class WatchPb
Throws:
ContradictionException

minWatchPbNew

public static MinWatchPb minWatchPbNew(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

minWatchPbNew

public static MinWatchPb minWatchPbNew(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

normalizedMinWatchPbNew

public static MinWatchPb normalizedMinWatchPbNew(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

normalizedMinWatchPbNew

public static MinWatchPb 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

nbOfWatched

protected int nbOfWatched()
Nombre de litt???raux actuellement observ???

Returns:
nombre de litt???raux regard???s

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???t???ct???e

remove

public void remove()
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???

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)

normalizedWatchPbNew

public static WatchPb normalizedWatchPbNew(ILits voc,
                                           IDataStructurePB mpb)

maximalCoefficient

protected java.math.BigInteger maximalCoefficient(int pIndice)
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)


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