|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectorg.sat4j.pb.constraints.pb.WatchPbLongCP
org.sat4j.pb.constraints.pb.MinWatchPbLongCP
public class MinWatchPbLongCP
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.
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.WatchPbLongCP |
---|
activity, bigCoefs, bigDegree, coefs, degree, learnt, lits, voc |
Constructor Summary | |
---|---|
protected |
MinWatchPbLongCP(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 |
MinWatchPbLongCP(ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree)
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 MinWatchPbLongCP |
normalizedMinWatchPbNew(UnitPropagationListener s,
ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree)
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 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.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, setLearnt, simplify, size, slackConstraint, slackConstraint, slackConstraint, sort, sort, toLong, toString |
Methods inherited from class java.lang.Object |
---|
clone, finalize, getClass, notify, notifyAll, wait, wait, wait |
Field Detail |
---|
protected long watchCumul
protected boolean[] watched
protected int[] watching
protected int watchingCount
Constructor Detail |
---|
protected MinWatchPbLongCP(ILits voc, IDataStructurePB mpb)
voc
- all the possible variables (vocabulary)mpb
- a mutable PB constraintprotected MinWatchPbLongCP(ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree)
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 |
---|
protected void computeWatches() throws ContradictionException
computeWatches
in class WatchPbLongCP
ContradictionException
protected void computePropagation(UnitPropagationListener s) throws ContradictionException
computePropagation
in class WatchPbLongCP
ContradictionException
public static MinWatchPbLongCP normalizedMinWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree) throws ContradictionException
s
- a unit propagation listenervoc
- the vocabularylits
- the literalscoefs
- the coefficientsdegree
- the degree of the constraint to normalize.
ContradictionException
protected int nbOfWatched()
public boolean propagate(UnitPropagationListener s, int p)
s
- the solverp
- the propagated literal (it must be falsified)
public void remove(UnitPropagationListener upl)
public void undo(int p)
p
- un unassigned literalpublic static WatchPbLongCP normalizedWatchPbNew(ILits voc, IDataStructurePB mpb)
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.
protected long maximalCoefficient(int pIndice)
pIndice
- propagated literal : its coefficient is excluded from the
search of the maximal coefficient
protected long updateWatched(long mc, int pIndice)
mc
- the current maximal coefficient of the watched literalspIndice
- the literal propagated (falsified)
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |