org.sat4j.minisat.constraints.card
Class MaxWatchCard

java.lang.Object
  extended by org.sat4j.minisat.constraints.card.MaxWatchCard
All Implemented Interfaces:
Serializable, Constr, Propagatable, Undoable, IConstr

public final class MaxWatchCard
extends Object
implements Constr, Undoable, Serializable

See Also:
Serialized Form

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'affection d'un litt?
 boolean canBePropagatedMultipleTimes()
          Partition constraints into the ones that can only be found once on the trail (e.g. clauses) and the ones that can be found several times (e.g.
 void forwardActivity(double claInc)
           
 int get(int i)
          returns the ith literal in the constraint
 double getActivity()
          Obtenir la valeur de l'activit?
 BigInteger getCoef(int literal)
           
 BigInteger getDegree()
           
 ILits getVocabulary()
           
 void incActivity(double claInc)
          Incr?
 boolean learnt()
          D?
 boolean locked()
          La contrainte est la cause d'une propagation unitaire
static Constr maxWatchCardNew(UnitPropagationListener s, ILits voc, IVecInt ps, boolean moreThan, int degree)
          Permet la cr?
 void normalize()
          On normalise la contrainte au sens de Barth
 boolean propagate(UnitPropagationListener s, int p)
          Propagation de la valeur de v?
 void register()
          Register the constraint to the solver.
 void remove(UnitPropagationListener upl)
          Remove a constraint from the solver.
 void rescaleBy(double d)
          Permet le r??
 void setLearnt()
          Mark a constraint as learnt.
 boolean simplify()
          Simplifie la contrainte(l'all?
 int size()
           
 String toString()
          Cha?
 void undo(int p)
          M?
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Method Detail

calcReason

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

Specified by:
calcReason in interface Constr
Parameters:
p - un litt?ral falsifi? (ou Lit.UNDEFINED)
outReason - vecteur de litt?raux ? remplir
See Also:
Constr.calcReason(int p, IVecInt outReason)

getActivity

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

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

incActivity

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

Specified by:
incActivity in interface Constr
Parameters:
claInc - incr?ment de l'activit? de la contrainte
See Also:
Constr.incActivity(double claInc)

learnt

public boolean learnt()
D?termine 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()

maxWatchCardNew

public static Constr maxWatchCardNew(UnitPropagationListener s,
                                     ILits voc,
                                     IVecInt ps,
                                     boolean moreThan,
                                     int degree)
                              throws ContradictionException
Permet la cr?ation de contrainte de cardinalit? ? observation minimale

Parameters:
s - outil pour la propagation des litt?raux
voc - vocabulaire utilis? par la contrainte
ps - liste des litt?raux de la nouvelle 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, null sinon
Throws:
ContradictionException

normalize

public final void normalize()
On normalise la contrainte au sens de Barth


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 - objet utilis? pour la propagation
p - le litt?ral propag? (il doit etre falsifie)
Returns:
false ssi une inconsistance est d?t?ct?e

remove

public void remove(UnitPropagationListener upl)
Description copied from interface: Constr
Remove a constraint from the solver.

Specified by:
remove in interface Constr
Since:
2.1

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

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

toString

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

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

undo

public void undo(int p)
M?thode appel?e lors du backtrack

Specified by:
undo in interface Undoable
Parameters:
p - le litt?ral d?saffect?

setLearnt

public void setLearnt()
Description copied from interface: Constr
Mark a constraint as learnt.

Specified by:
setLearnt in interface Constr

register

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

Specified by:
register in interface Constr

size

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

get

public int get(int i)
Description copied from interface: IConstr
returns the ith literal in the constraint

Specified by:
get in interface IConstr
Parameters:
i - the index of the literal
Returns:
a literal

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.

getCoef

public BigInteger getCoef(int literal)

getDegree

public BigInteger getDegree()

getVocabulary

public ILits getVocabulary()

forwardActivity

public void forwardActivity(double claInc)
Specified by:
forwardActivity in interface Constr
Since:
2.1

canBePropagatedMultipleTimes

public boolean canBePropagatedMultipleTimes()
Description copied from interface: IConstr
Partition constraints into the ones that can only be found once on the trail (e.g. clauses) and the ones that can be found several times (e.g. cardinality constraints and pseudo-boolean constraints).

Specified by:
canBePropagatedMultipleTimes in interface IConstr
Returns:
true if the constraint can be used several times as a reason to propagate a literal.


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