org.sat4j.pb.constraints.pb
Class MinWatchPbLong

java.lang.Object
  extended by org.sat4j.pb.constraints.pb.WatchPbLong
      extended by org.sat4j.pb.constraints.pb.MinWatchPbLong
All Implemented Interfaces:
Serializable, Constr, Propagatable, Undoable, IConstr

public class MinWatchPbLong
extends WatchPbLong

Data structure for pseudo-boolean constraint with watched literals. All literals are watched. The sum of the literals satisfied or unvalued is always memorized, to detect conflict.

See Also:
Serialized Form

Field Summary
protected  long watchCumul
          sum of the coefficients of the literals satisfied or unvalued
protected  boolean[] watched
          is the literal of index i watching the constraint ?
protected  int[] watching
          indexes of literals watching the constraint
protected  int watchingCount
          number of literals watching the constraint.
 
Fields inherited from class org.sat4j.pb.constraints.pb.WatchPbLong
activity, coefs, degree, learnt, lits, sumcoefs, voc
 
Constructor Summary
protected MinWatchPbLong(ILits voc, IDataStructurePB mpb)
          Basic constructor for pb constraint a0.x0 + a1.x1 + ... + an.xn >= k This constructor is called for learnt pseudo boolean constraints.
protected MinWatchPbLong(ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs)
          Basic constructor for PB constraint a0.x0 + a1.x1 + ... + an.xn >= k
 
Method Summary
protected  void computePropagation(UnitPropagationListener s)
           
protected  void computeWatches()
           
protected  long maximalCoefficient(int pIndice)
          the maximal coefficient for the watched literals
protected  int nbOfWatched()
          Number of really watched literals.
static MinWatchPbLong normalizedMinWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs)
          build a pseudo boolean constraint.
static WatchPbLong normalizedWatchPbNew(ILits voc, IDataStructurePB mpb)
          build a pseudo boolean constraint from a specific data structure.
 boolean propagate(UnitPropagationListener s, int p)
          Propagation of a falsified literal
 void remove(UnitPropagationListener upl)
          Remove the constraint from the solver
 void undo(int p)
          this method is called during backtrack
protected  long updateWatched(long mc, int pIndice)
          update arrays watched and watching w.r.t. the propagation of a literal.
 
Methods inherited from class org.sat4j.pb.constraints.pb.WatchPbLong
assertConstraint, calcReason, canBePropagatedMultipleTimes, coefficientsEqualToOne, computeAnImpliedClause, computeLeftSide, computeLeftSide, equals, forwardActivity, get, getActivity, getLits, getVocabulary, hashCode, incActivity, isAssertive, isSatisfiable, learnt, locked, ppcm, register, rescaleBy, setActivity, setLearnt, simplify, size, slackConstraint, slackConstraint, sort, sort, toConstraint, toLong, toString
 
Methods inherited from class java.lang.Object
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
 

Field Detail

watchCumul

protected long watchCumul
sum of the coefficients of the literals satisfied or unvalued


watched

protected boolean[] watched
is the literal of index i watching the constraint ?


watching

protected int[] watching
indexes of literals watching the constraint


watchingCount

protected int watchingCount
number of literals watching the constraint. This is the real size of the array watching

Constructor Detail

MinWatchPbLong

protected MinWatchPbLong(ILits voc,
                         IDataStructurePB mpb)
Basic constructor for pb constraint a0.x0 + a1.x1 + ... + an.xn >= k This constructor is called for learnt pseudo boolean constraints.

Parameters:
voc - all the possible variables (vocabulary)
mpb - a mutable PB constraint

MinWatchPbLong

protected MinWatchPbLong(ILits voc,
                         int[] lits,
                         BigInteger[] coefs,
                         BigInteger degree,
                         BigInteger sumCoefs)
Basic constructor for PB constraint a0.x0 + a1.x1 + ... + an.xn >= k

Parameters:
voc - all the possible variables (vocabulary)
lits - literals of the constraint (x0,x1, ... xn)
coefs - coefficients of the left side of the constraint (a0, a1, ... an)
degree - degree of the constraint (k)
Method Detail

computeWatches

protected void computeWatches()
                       throws ContradictionException
Specified by:
computeWatches in class WatchPbLong
Throws:
ContradictionException

computePropagation

protected void computePropagation(UnitPropagationListener s)
                           throws ContradictionException
Specified by:
computePropagation in class WatchPbLong
Throws:
ContradictionException

normalizedMinWatchPbNew

public static MinWatchPbLong normalizedMinWatchPbNew(UnitPropagationListener s,
                                                     ILits voc,
                                                     int[] lits,
                                                     BigInteger[] coefs,
                                                     BigInteger degree,
                                                     BigInteger sumCoefs)
                                              throws ContradictionException
build a pseudo boolean constraint. Coefficients are positive integers less than or equal to the degree (this is called a normalized constraint).

Parameters:
s - a unit propagation listener
voc - the vocabulary
lits - the literals
coefs - the coefficients
degree - the degree of the constraint to normalize.
Returns:
a new PB constraint or null if a trivial inconsistency is detected.
Throws:
ContradictionException

nbOfWatched

protected int nbOfWatched()
Number of really watched literals. It should return the same value as watchingCount. This method must only be called for assertions.

Returns:
number of watched literals.

propagate

public boolean propagate(UnitPropagationListener s,
                         int p)
Propagation of a falsified literal

Specified by:
propagate in interface Propagatable
Overrides:
propagate in class WatchPbLong
Parameters:
s - the solver
p - the propagated literal (it must be falsified)
Returns:
false iff there is a conflict

remove

public void remove(UnitPropagationListener upl)
Remove the constraint from the solver

Specified by:
remove in interface Constr
Overrides:
remove in class WatchPbLong

undo

public void undo(int p)
this method is called during backtrack

Specified by:
undo in interface Undoable
Overrides:
undo in class WatchPbLong
Parameters:
p - un unassigned literal

normalizedWatchPbNew

public static WatchPbLong normalizedWatchPbNew(ILits voc,
                                               IDataStructurePB mpb)
build a pseudo boolean constraint from a specific data structure. For learnt constraints.

Parameters:
s - a unit propagation listener (usually the solver)
mpb - data structure which contains literals of the constraint, coefficients (a0, a1, ... an), and the degree of the constraint (k). The constraint is a "more than" constraint.
Returns:
a new PB constraint or null if a trivial inconsistency is detected.

maximalCoefficient

protected long maximalCoefficient(int pIndice)
the maximal coefficient for the watched literals

Parameters:
pIndice - propagated literal : its coefficient is excluded from the search of the maximal coefficient
Returns:
the maximal coefficient for the watched literals

updateWatched

protected long updateWatched(long mc,
                             int pIndice)
update arrays watched and watching w.r.t. the propagation of a literal. return the maximal coefficient of the watched literals (could have been changed).

Parameters:
mc - the current maximal coefficient of the watched literals
pIndice - the literal propagated (falsified)
Returns:
the new maximal coefficient of the watched literals


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