org.sat4j.minisat.constraints.pb
Class WatchPb

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

All Implemented Interfaces:

Constr, Propagatable, Undoable, IConstr

Direct Known Subclasses:

MaxWatchPb, MinWatchPb

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

Field Summary

static boolean	ATLEAST
static boolean	ATMOST Constante pour le type d'in?

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???
int	get(int i) Permet d'obtenir le i-???
double	getActivity() Obtenir la valeur de l'activit???
int	getBacktrackLevel(int maxLevel) retourne le niveau de backtrack : c'est-?
java.math.BigInteger	getCoef(int i) Permet d'obtenir le i-???
java.math.BigInteger	getDegree()
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
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
java.lang.String	toString() Cha???

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

Constante pour le type d'in?galit?

See Also:

Constant Field Values

ATLEAST

public static final boolean ATLEAST

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

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

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

getBacktrackLevel

public int getBacktrackLevel(int maxLevel)

retourne le niveau de backtrack : c'est-?-dire le niveau le plus haut pour lequel la contrainte est assertive

Parameters:

maxLevel - le plus bas niveau pour lequel la contrainte est assertive

Returns:

the highest level (smaller int) for which the constraint is assertive.

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

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