org.sat4j.minisat.constraints.card
Class MinWatchCard

java.lang.Object
  extended by org.sat4j.minisat.constraints.card.MinWatchCard
All Implemented Interfaces:
Serializable, Constr, Propagatable, Undoable, IConstr

public class MinWatchCard
extends Object
implements Constr, Undoable, Serializable

See Also:
Serialized Form

Field Summary
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
  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
 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
 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 setLearnt()
          Mark a constraint as learnt.
 boolean simplify()
          simplifies the constraint
 int size()
           
 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)

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

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.


Copyright © 2011 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.