org.sat4j.pb.constraints.pb
Class MaxWatchPbLongCP

java.lang.Object
  extended by org.sat4j.pb.constraints.pb.WatchPbLongCP
      extended by org.sat4j.pb.constraints.pb.MaxWatchPbLongCP
All Implemented Interfaces:
Serializable, Constr, Propagatable, Undoable, IWatchPb, PBConstr, IConstr

public final class MaxWatchPbLongCP
extends WatchPbLongCP

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
 
Fields inherited from class org.sat4j.pb.constraints.pb.WatchPbLongCP
activity, bigCoefs, bigDegree, coefs, degree, learnt, lits, sumcoefs, voc
 
Method Summary
protected  void computePropagation(UnitPropagationListener s)
           
protected  void computeWatches()
          All the literals are watched.
static MaxWatchPbLongCP normalizedMaxWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs)
          build a pseudo boolean constraint.
static WatchPbLongCP 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 a constraint from the solver
 void undo(int p)
          this method is called during backtrack
 
Methods inherited from class org.sat4j.pb.constraints.pb.WatchPbLongCP
assertConstraint, calcReason, canBePropagatedMultipleTimes, coefficientsEqualToOne, computeAnImpliedClause, computeLeftSide, computeLeftSide, computeLeftSide, equals, forwardActivity, get, getActivity, getCoef, getCoefs, getDegree, getLits, getLongCoefs, getVocabulary, hashCode, incActivity, isAssertive, isSatisfiable, learnt, locked, ppcm, register, rescaleBy, setActivity, setLearnt, simplify, size, slackConstraint, slackConstraint, slackConstraint, sort, sort, toConstraint, toLong, toString
 
Methods inherited from class java.lang.Object
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
 

Method Detail

computeWatches

protected void computeWatches()
                       throws ContradictionException
All the literals are watched.

Specified by:
computeWatches in class WatchPbLongCP
Throws:
ContradictionException
See Also:
WatchPbLong.computeWatches()

computePropagation

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

propagate

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

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 a constraint from the solver


undo

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

Parameters:
p - an unassigned literal

normalizedMaxWatchPbNew

public static MaxWatchPbLongCP normalizedMaxWatchPbNew(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 (usually the solver)
voc - the vocabulary
lits - the literals of the constraint
coefs - the coefficients of the constraint
degree - the degree of the constraint
Returns:
a new PB constraint or null if a trivial inconsistency is detected.
Throws:
ContradictionException

normalizedWatchPbNew

public static WatchPbLongCP 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.


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