org.sat4j.minisat.constraints.card

Class MinWatchCard

java.lang.Object

org.sat4j.minisat.constraints.card.MinWatchCard

All Implemented Interfaces:

Serializable, Constr, Propagatable, Undoable, IConstr

public class MinWatchCard
extends Object
implements Propagatable, Constr, Undoable, Serializable

See Also:

Serialized Form

Field Summary

Fields

Modifier and Type	Field and Description
static boolean	ATLEAST
static boolean	ATMOST
protected int	degree degree of the cardinality constraint
protected int	watchCumul contains the sum of the coefficients of the watched literals

Constructor Summary

Constructors

Modifier	Constructor and Description
	MinWatchCard(ILits voc, IVecInt ps, boolean moreThan, int degree) Constructs and normalizes a cardinality constraint. used by minWatchCardNew in the non-normalized case.
protected	MinWatchCard(ILits voc, IVecInt ps, int degree) Constructs and normalizes a cardinality constraint. used by MinWatchCardPB.normalizedMinWatchCardNew() in the normalized case.

Method Summary

Methods

Modifier and Type	Method and Description
void	assertConstraint(UnitPropagationListener s) Method called when the constraint is to be asserted.
void	assertConstraintIfNeeded(UnitPropagationListener s) Method called when the constraint is added to the solver "on the fly".
void	calcReason(int p, IVecInt outReason) computes the reason for a literal
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.
protected MinWatchCard	computePropagation(UnitPropagationListener s)
protected void	computeWatches()
boolean	equals(Object card)
void	forwardActivity(double claInc)
int	get(int i) returns the ith literal in the constraint
double	getActivity() Returns the activity of the constraint
int[]	getLits()
ILits	getVocabulary()
int	hashCode()
void	incActivity(double claInc) Increments activity of the constraint
boolean	learnt() Returns wether the constraint is learnt or not.
protected static int	linearisation(ILits voc, IVecInt ps) Simplifies the constraint w.r.t. the assignments of the literals
boolean	locked() Returns if the constraint is the reason for a unit propagation.
static Constr	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(UnitPropagationListener upl) Removes a constraint from the solver
void	rescaleBy(double d) Rescales the activity value of the constraint
void	setActivity(double d) Set the activity at a specific value
void	setLearnt() Mark a constraint as learnt.
boolean	simplify() simplifies the constraint
int	size()
Constr	toConstraint() Allow to access a constraint view of the propagatable to avoid casting.
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

clone, finalize, getClass, 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

degree

protected int degree

degree of the cardinality constraint

watchCumul

protected int watchCumul

contains the sum of the coefficients of the watched literals

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

MinWatchCard

protected MinWatchCard(ILits voc,
            IVecInt ps,
            int degree)

Constructs and normalizes a cardinality constraint. used by MinWatchCardPB.normalizedMinWatchCardNew() in the normalized case.
Should not be used if parameters are not already normalized
This constraint is always an ATLEAST constraint.

Parameters:

voc - vocabulary used by the constraint

ps - literals involved in the constraint

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 IConstr

Returns:

activity value of the constraint

See Also:

IConstr.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)

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

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

linearisation

protected static int linearisation(ILits voc,
                IVecInt ps)

Simplifies the constraint w.r.t. the assignments of the literals

Parameters:

voc - vocabulary used

ps - literals involved

Returns:

value to be added to the degree. This value is less than or equal to 0.

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 Constr 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(UnitPropagationListener upl)

Removes a constraint from the solver

Specified by:

remove in interface Constr

Since:

2.1

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

Returns a string representation of the constraint.

Overrides:

toString in class 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 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.

assertConstraintIfNeeded

public void assertConstraintIfNeeded(UnitPropagationListener s)

Description copied from interface: Constr

Method called when the constraint is added to the solver "on the fly". In that case, the constraint may or may not have to propagate some literals, unlike the Constr.assertConstraint(UnitPropagationListener) method.

Specified by:

assertConstraintIfNeeded in interface Constr

Parameters:

s - a UnitPropagationListener to use for unit propagation.

computeWatches

protected void computeWatches()

computePropagation

protected MinWatchCard computePropagation(UnitPropagationListener s)
                                   throws ContradictionException

Throws:

ContradictionException

getLits

public int[] getLits()

getVocabulary

public ILits getVocabulary()

equals

public boolean equals(Object card)

Overrides:

equals in class Object

hashCode

public int hashCode()

Overrides:

hashCode in class Object

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.