org.sat4j.minisat.constraints.card
Class MaxWatchCard

java.lang.Object
  org.sat4j.minisat.constraints.card.MaxWatchCard

All Implemented Interfaces:

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

public class MaxWatchCard
extends java.lang.Object
implements Constr, Undoable, java.io.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?
int	get(int i) returns the ith literal in the constraint
double	getActivity() Obtenir la valeur de l'activit?
java.math.BigInteger	getCoef(int literal)
java.math.BigInteger	getDegree()
ILits	getVocabulary()
void	incActivity(double claInc) Incr?
boolean	learnt() D?
boolean	locked() La contrainte est la cause d'une propagation unitaire
static MaxWatchCard	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() Enl?
void	rescaleBy(double d) Permet le r??
void	setLearnt() Mark a constraint as learnt.
boolean	simplify() Simplifie la contrainte(l'all?
int	size()
java.lang.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 Constr

Returns:

la valeur de l'activit? de la contrainte

See Also:

Constr.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 MaxWatchCard 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()

Enl?ve une contrainte du prouveur

Specified by:

remove in interface Constr

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 java.lang.String toString()

Cha?ne repr?sentant la contrainte

Overrides:

toString in class java.lang.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 java.math.BigInteger getCoef(int literal)

getDegree

public java.math.BigInteger getDegree()

getVocabulary

public ILits getVocabulary()