org.sat4j.minisat.constraints.card

Class MaxWatchCard

java.lang.Object

org.sat4j.minisat.constraints.card.MaxWatchCard

All Implemented Interfaces:

Serializable, Constr, Propagatable, Undoable, IConstr

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

See Also:

Serialized Form

Constructor Summary

Constructors

Constructor and Description
MaxWatchCard(ILits voc, IVecInt ps, boolean moreThan, int degree) Constructeur de base cr?

Method Summary

Methods

Modifier and Type	Method and Description
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?
void	calcReasonOnTheFly(int p, IVecInt trail, IVecInt outReason) Compute the reason for a given assignment in a the constraint created on the fly in the solver.
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	setActivity(double d) Set the activity at a specific value
void	setLearnt() Mark a constraint as learnt.
boolean	simplify() Simplifie la contrainte(l'all?
int	size()
Constr	toConstraint() Allow to access a constraint view of the propagatable to avoid casting.
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

Constructor Detail

MaxWatchCard

public MaxWatchCard(ILits voc,
            IVecInt ps,
            boolean moreThan,
            int degree)

Constructeur de base cr?ant des contraintes vides

Parameters:

size - nombre de litt?raux de la contrainte

learnt - indique si la contrainte est apprise

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)

setActivity

public void setActivity(double d)

Description copied from interface: Constr

Set the activity at a specific value

Specified by:

setActivity in interface Constr

Parameters:

d - the new activity

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 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 learned 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.

toConstraint

public Constr toConstraint()

Description copied from interface: Propagatable

Allow to access a constraint view of the propagatable to avoid casting. In most cases, the constraint will implement directly propagatable thus will return itself. It will also also the implementation of more sophisticated watching strategy.

Specified by:

toConstraint in interface Propagatable

Returns:

the constraint associated to that propagatable.

calcReasonOnTheFly

public void calcReasonOnTheFly(int p,
                      IVecInt trail,
                      IVecInt outReason)

Description copied from interface: Constr

Compute the reason for a given assignment in a the constraint created on the fly in the solver. Compared to the method Constr.calcReason(int, IVecInt), the falsification may not have been detected as soon as possible. As such, it is necessary to take into account the order of the literals in the trail.

Specified by:

calcReasonOnTheFly in interface Constr

Parameters:

p - a satisfied literal (or Lit.UNDEFINED)

trail - all the literals satisfied in the solvers, should not be modified.

outReason - a list of falsified literals whose negation is the reason of the assignment of p to true.