org.sat4j.minisat.constraints.card
Class AtLeast

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

All Implemented Interfaces:

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

Direct Known Subclasses:

AtLeastPB

public class AtLeast
extends java.lang.Object
implements Constr, Undoable, java.io.Serializable

Author:

leberre Contrainte de cardinalit?

See Also:

Serialized Form

Method Summary

void	assertConstraint(UnitPropagationListener s) Method called when the constraint is to be asserted.
static AtLeast	atLeastNew(UnitPropagationListener s, ILits voc, IVecInt ps, int n)
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()
void	incActivity(double claInc)
boolean	learnt()
boolean	locked() Indicate wether a constraint is responsible from an assignment.
boolean	propagate(UnitPropagationListener s, int p) Propagate the truth value of a literal in constraints in which that literal is falsified.
void	register() Register the constraint to the solver.
void	remove() Enl?
void	rescaleBy(double d) Rescale the clause activity by a value.
void	setLearnt() Mark a constraint as learnt.
boolean	simplify() Simplifie une contrainte, par exemple en enlevant les litt?
int	size()
java.lang.String	toString() Cha?
void	undo(int p) M?

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

Method Detail

atLeastNew

public static AtLeast atLeastNew(UnitPropagationListener s,
                                 ILits voc,
                                 IVecInt ps,
                                 int n)
                          throws ContradictionException

Throws:

ContradictionException

remove

public void remove()

Description copied from interface: Constr

Enl?ve une contrainte du prouveur

Specified by:

remove in interface Constr

propagate

public boolean propagate(UnitPropagationListener s,
                         int p)

Description copied from interface: Propagatable

Propagate the truth value of a literal in constraints in which that literal is falsified.

Specified by:

propagate in interface Propagatable

Parameters:

s - something able to perform unit propagation

p - the literal being propagated. Its negation must appear in the constraint.

Returns:

false iff an inconsistency (a contradiction) is detected.

simplify

public boolean simplify()

Description copied from interface: Constr

Simplifie une contrainte, par exemple en enlevant les litt?raux falsifi?s.

Specified by:

simplify in interface Constr

Returns:

true ssi la contrainte est satisfaite.

undo

public void undo(int p)

Description copied from interface: Undoable

M?thode appel?e lors du backtrack

Specified by:

undo in interface Undoable

Parameters:

p - un litt?ral d?saffect?

calcReason

public void calcReason(int p,
                       IVecInt outReason)

Description copied from interface: Constr

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 - la liste des litt?raux falsifi?s dont la n?gation correspond ? la raison de l'affectation.

learnt

public boolean learnt()

Specified by:

learnt in interface IConstr

Returns:

true iff the clause was learnt during the search

getActivity

public double getActivity()

Specified by:

getActivity in interface Constr

Returns:

the activity of the clause.

incActivity

public void incActivity(double claInc)

Specified by:

incActivity in interface Constr

Parameters:

claInc - the value to increase the activity with

locked

public boolean locked()

Description copied from interface: Constr

Indicate wether a constraint is responsible from an assignment.

Specified by:

locked in interface Constr

Returns:

true if a constraint is a "reason" for an assignment.

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

rescaleBy

public void rescaleBy(double d)

Description copied from interface: Constr

Rescale the clause activity by a value.

Specified by:

rescaleBy in interface Constr

Parameters:

d - the value to rescale the clause activity with.

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.

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