org.sat4j.minisat.constraints.card
Class MinWatchCard

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

All Implemented Interfaces:

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

Direct Known Subclasses:

MinWatchCardPB

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

See Also:

Serialized Form

Field Summary

static boolean	ATLEAST
static boolean	ATMOST

Constructor Summary

MinWatchCard(ILits voc, IVecInt ps, boolean moreThan, int degree)
Constructs and normalizes a cardinality constraint.

Method Summary

void	assertConstraint(UnitPropagationListener s) Method called when the constraint is to be asserted.
void	calcReason(int p, IVecInt outReason) computes the reason for a literal
int	get(int i) returns the ith literal in the constraint
double	getActivity() Returns the activity of the constraint
int[]	getLits()
ILits	getVocabulary()
void	incActivity(double claInc) Increments activity of the constraint
boolean	learnt() Returns wether the constraint is learnt or not.
boolean	locked() Returns if the constraint is the reason for a unit propagation.
static MinWatchCard	minWatchCardNew(UnitPropagationListener s, ILits voc, IVecInt ps, boolean moreThan, int degree) Constructs a cardinality constraint with a minimal set of watched literals Permet la cr?
void	normalize() normalize the constraint (cf.
boolean	propagate(UnitPropagationListener s, int p) propagates the value of a falsified literal
void	register() Register the constraint to the solver.
void	remove() Removes a constraint from the solver
void	rescaleBy(double d) Rescales the activity value of the constraint
void	setLearnt() Mark a constraint as learnt.
boolean	simplify() simplifies the constraint
int	size()
java.lang.String	toString() Returns a string representation of the constraint.
void	undo(int p) Updates information on the constraint in case of a backtrack

Methods inherited from class java.lang.Object

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

Field Detail

ATLEAST

public static final boolean ATLEAST

See Also:

Constant Field Values

ATMOST

public static final boolean ATMOST

See Also:

Constant Field Values

Constructor Detail

MinWatchCard

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

Constructs and normalizes a cardinality constraint. used by minWatchCardNew in the non-normalized case.

Parameters:

voc - vocabulary used by the constraint

ps - literals involved in the constraint

moreThan - should be ATLEAST or ATMOST;

degree - degree of the constraint

Method Detail

calcReason

public void calcReason(int p,
                       IVecInt outReason)

computes the reason for a literal

Specified by:

calcReason in interface Constr

Parameters:

p - falsified literal (or Lit.UNDEFINED)

outReason - the reason to be computed. Vector of literals.

See Also:

Constr.calcReason(int p, IVecInt outReason)

getActivity

public double getActivity()

Returns the activity of the constraint

Specified by:

getActivity in interface Constr

Returns:

activity value of the constraint

See Also:

Constr.getActivity()

incActivity

public void incActivity(double claInc)

Increments activity of the constraint

Specified by:

incActivity in interface Constr

Parameters:

claInc - value to be added to the activity of the constraint

See Also:

Constr.incActivity(double claInc)

learnt

public boolean learnt()

Returns wether the constraint is learnt or not.

Specified by:

learnt in interface IConstr

Returns:

false : a MinWatchCard cannot be learnt.

See Also:

IConstr.learnt()

locked

public boolean locked()

Returns if the constraint is the reason for a unit propagation.

Specified by:

locked in interface Constr

Returns:

true

See Also:

Constr.locked()

minWatchCardNew

public static MinWatchCard minWatchCardNew(UnitPropagationListener s,
                                           ILits voc,
                                           IVecInt ps,
                                           boolean moreThan,
                                           int degree)
                                    throws ContradictionException

Constructs a cardinality constraint with a minimal set of watched literals Permet la cr?ation de contrainte de cardinalit? ? observation minimale

Parameters:

s - tool for propagation

voc - vocalulary used by the constraint

ps - literals involved in the constraint

moreThan - sign of the constraint. Should be ATLEAST or ATMOST.

degree - degree of the constraint

Returns:

a new cardinality constraint, null if it is a tautology

Throws:

ContradictionException

normalize

public final void normalize()

normalize the constraint (cf. P.Barth normalization)

propagate

public boolean propagate(UnitPropagationListener s,
                         int p)

propagates the value of a falsified literal

Specified by:

propagate in interface Propagatable

Parameters:

s - tool for literal propagation

p - falsified literal

Returns:

false if an inconistency is detected, else true

remove

public void remove()

Removes a constraint from the solver

Specified by:

remove in interface Constr

rescaleBy

public void rescaleBy(double d)

Rescales the activity value of the constraint

Specified by:

rescaleBy in interface Constr

Parameters:

d - rescale factor

simplify

public boolean simplify()

simplifies the constraint

Specified by:

simplify in interface Constr

Returns:

true if the constraint is satisfied, else false

toString

public java.lang.String toString()

Returns a string representation of the constraint.

Overrides:

toString in class java.lang.Object

Returns:

representation of the constraint.

undo

public void undo(int p)

Updates information on the constraint in case of a backtrack

Specified by:

undo in interface Undoable

Parameters:

p - unassigned literal

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.

getLits

public int[] getLits()

getVocabulary

public ILits getVocabulary()