org.sat4j.minisat.constraints.pb
Class WatchPb

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

public abstract class WatchPb
extends java.lang.Object
implements PBConstr, Undoable


Field Summary
static boolean ATLEAST
          constant for the initial type of inequality more than or equal
static boolean ATMOST
          constant for the initial type of inequality less than or equal
 
Method Summary
 void assertConstraint(UnitPropagationListener s)
          Method called when the constraint is to be asserted.
 void calcReason(int p, IVecInt outReason)
          Calcule la cause de l'affectation d'un litt???
 boolean coefficientsEqualToOne()
           
 IVecInt computeAnImpliedClause()
          compute an implied clause on the literals with the greater coefficients
 int get(int i)
          Permet d'obtenir le i-???
 double getActivity()
          Obtenir la valeur de l'activit???
 java.math.BigInteger getCoef(int i)
          Permet d'obtenir le i-???
 java.math.BigInteger[] getCoefs()
           
 java.math.BigInteger getDegree()
           
 int[] getLits()
           
 ILits getVocabulary()
           
 void incActivity(double claInc)
          Incr???
 boolean isAssertive(int dl)
          teste si la contrainte est assertive au niveau de d?
 boolean learnt()
          Dit si la contrainte est apprise
 boolean locked()
          La contrainte est la cause d'une propagation unitaire
static IDataStructurePB niceCheckedParameters(IVecInt ps, IVec<java.math.BigInteger> bigCoefs, boolean moreThan, java.math.BigInteger bigDeg, ILits voc)
           
static IDataStructurePB niceParameters(IVecInt ps, IVec<java.math.BigInteger> bigCoefs, boolean moreThan, java.math.BigInteger bigDeg, ILits voc)
           
 java.math.BigInteger recalcLeftSide()
          somme des coefficients des litteraux satisfaits ou non assignes de la resolvante
 java.math.BigInteger recalcLeftSide(java.math.BigInteger[] coefs)
          somme des coefficients des litteraux satisfaits ou non assignes de la resolvante
 void register()
          Register the constraint to the solver.
 void rescaleBy(double d)
          Permet le r??????
 void setLearnt()
          La contrainte est apprise
 boolean simplify()
          Simplifie la contrainte(l'all???
 int size()
           
 java.math.BigInteger slackConstraint()
          Marge de la contrainte courante marge = poss - degre de la contrainte
 java.math.BigInteger slackConstraint(java.math.BigInteger[] coefs, java.math.BigInteger degree)
          Marge de la contrainte courante marge = poss - degre de la contrainte
static java.math.BigInteger toBigInt(int i)
           
 java.lang.String toString()
          Cha???
static IVec<java.math.BigInteger> toVecBigInt(IVecInt vec)
           
 
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, wait, wait, wait
 
Methods inherited from interface org.sat4j.minisat.core.Constr
remove
 
Methods inherited from interface org.sat4j.minisat.core.Propagatable
propagate
 
Methods inherited from interface org.sat4j.minisat.core.Undoable
undo
 

Field Detail

ATMOST

public static final boolean ATMOST
constant for the initial type of inequality less than or equal

See Also:
Constant Field Values

ATLEAST

public static final boolean ATLEAST
constant for the initial type of inequality more than or equal

See Also:
Constant Field Values
Method Detail

isAssertive

public boolean isAssertive(int dl)
teste si la contrainte est assertive au niveau de d?cision > dl

Parameters:
dl -
Returns:
true iff the constraint is assertive at decision level dl.

calcReason

public void calcReason(int p,
                       IVecInt outReason)
Calcule la cause de l'affectation d'un litt???ral

Specified by:
calcReason in interface Constr
Parameters:
p - un litt???ral falsifi??? (ou Lit.UNDEFINED)
outReason - la liste des litt???raux falsifi???s dont la n???gation correspond ??? la raison de l'affectation.
See Also:
Constr.calcReason(int, IVecInt)

get

public int get(int i)
Permet d'obtenir le i-???me litt???ral de la contrainte

Specified by:
get in interface IConstr
Parameters:
i - indice du litt???ral recherch???
Returns:
le litt???ral demand???

getCoef

public java.math.BigInteger getCoef(int i)
Permet d'obtenir le i-???me litt???ral de la contrainte

Specified by:
getCoef in interface PBConstr
Parameters:
i - indice du litt???ral recherch???
Returns:
le litt???ral demand???

getActivity

public double getActivity()
Obtenir la valeur de l'activit??? de la contrainte

Specified by:
getActivity in interface Constr
Returns:
la valeur de l'activit??? de la contrainte
See Also:
Constr.getActivity()

niceParameters

public static IDataStructurePB niceParameters(IVecInt ps,
                                              IVec<java.math.BigInteger> bigCoefs,
                                              boolean moreThan,
                                              java.math.BigInteger bigDeg,
                                              ILits voc)
                                       throws ContradictionException
Throws:
ContradictionException

niceCheckedParameters

public static IDataStructurePB niceCheckedParameters(IVecInt ps,
                                                     IVec<java.math.BigInteger> bigCoefs,
                                                     boolean moreThan,
                                                     java.math.BigInteger bigDeg,
                                                     ILits voc)

incActivity

public void incActivity(double claInc)
Incr???mente la valeur de l'activit??? de la contrainte

Specified by:
incActivity in interface Constr
Parameters:
claInc - the value to increase the activity with
See Also:
Constr.incActivity(double claInc)

slackConstraint

public java.math.BigInteger slackConstraint()
Marge de la contrainte courante marge = poss - degre de la contrainte

Returns:
la marge

slackConstraint

public java.math.BigInteger slackConstraint(java.math.BigInteger[] coefs,
                                            java.math.BigInteger degree)
Marge de la contrainte courante marge = poss - degre de la contrainte

Parameters:
coefs - le tableau des coefficients de la contrainte consideree
degree - le degre de la contrainte consideree
Returns:
la marge

recalcLeftSide

public java.math.BigInteger recalcLeftSide(java.math.BigInteger[] coefs)
somme des coefficients des litteraux satisfaits ou non assignes de la resolvante

Parameters:
coefs - le tableau des coefficients de la contrainte consid?r?e
Returns:
cette somme (poss)

recalcLeftSide

public java.math.BigInteger recalcLeftSide()
somme des coefficients des litteraux satisfaits ou non assignes de la resolvante

Returns:
cette somme (poss)

learnt

public boolean learnt()
Dit si la contrainte est apprise

Specified by:
learnt in interface IConstr
Returns:
true si la contrainte est apprise, false sinon
See Also:
IConstr.learnt()

locked

public boolean locked()
La contrainte est la cause d'une propagation unitaire

Specified by:
locked in interface Constr
Returns:
true si c'est le cas, false sinon
See Also:
Constr.locked()

rescaleBy

public void rescaleBy(double d)
Permet le r??????chantillonage de l'activit??? de la contrainte

Specified by:
rescaleBy in interface Constr
Parameters:
d - facteur d'ajustement

setLearnt

public void setLearnt()
La contrainte est apprise

Specified by:
setLearnt in interface Constr

simplify

public boolean simplify()
Simplifie la contrainte(l'all???ge)

Specified by:
simplify in interface Constr
Returns:
true si la contrainte est satisfaite, false sinon

size

public int size()
Specified by:
size in interface IConstr
Returns:
the number of literals in the constraint.

toString

public java.lang.String toString()
Cha???ne repr???sentant la contrainte

Overrides:
toString in class java.lang.Object
Returns:
Cha???ne repr???sentant la contrainte

assertConstraint

public void assertConstraint(UnitPropagationListener s)
Description copied from interface: Constr
Method called when the constraint is to be asserted. It means that the constraint was learnt during the search and it should now propagate some truth values. In the clausal case, only one literal should be propagated. In other cases, it might be different.

Specified by:
assertConstraint in interface Constr
Parameters:
s - a UnitPropagationListener to use for unit propagation.

getDegree

public java.math.BigInteger getDegree()
Specified by:
getDegree in interface PBConstr
Returns:
Returns the degree.

register

public void register()
Description copied from interface: Constr
Register the constraint to the solver.

Specified by:
register in interface Constr

toVecBigInt

public static IVec<java.math.BigInteger> toVecBigInt(IVecInt vec)

toBigInt

public static java.math.BigInteger toBigInt(int i)

getCoefs

public java.math.BigInteger[] getCoefs()
Specified by:
getCoefs in interface PBConstr

getLits

public int[] getLits()
Specified by:
getLits in interface PBConstr

getVocabulary

public ILits getVocabulary()
Specified by:
getVocabulary in interface PBConstr

computeAnImpliedClause

public IVecInt computeAnImpliedClause()
compute an implied clause on the literals with the greater coefficients

Specified by:
computeAnImpliedClause in interface PBConstr

coefficientsEqualToOne

public boolean coefficientsEqualToOne()