|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object org.sat4j.pb.constraints.pb.WatchPbLong org.sat4j.pb.constraints.pb.MinWatchPbLongLimit
public class MinWatchPbLongLimit
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 |
compWatchCumul
if watchCumul is at Long.MAX_VALUE, contains the complement to the sum of the coefficients of the literals satisfied or unvalued |
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 |
MinWatchPbLongLimit(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 |
MinWatchPbLongLimit(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 MinWatchPbLongLimit |
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 |
---|
protected long watchCumul
protected long compWatchCumul
protected boolean[] watched
protected int[] watching
protected int watchingCount
Constructor Detail |
---|
protected MinWatchPbLongLimit(ILits voc, IDataStructurePB mpb)
voc
- all the possible variables (vocabulary)mpb
- a mutable PB constraintprotected MinWatchPbLongLimit(ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs)
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 WatchPbLong
ContradictionException
protected void computePropagation(UnitPropagationListener s) throws ContradictionException
computePropagation
in class WatchPbLong
ContradictionException
public static MinWatchPbLongLimit normalizedMinWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs) 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)
propagate
in interface Propagatable
propagate
in class WatchPbLong
s
- the solverp
- the propagated literal (it must be falsified)
public void remove(UnitPropagationListener upl)
remove
in interface Constr
remove
in class WatchPbLong
public void undo(int p)
undo
in interface Undoable
undo
in class WatchPbLong
p
- un unassigned literalpublic static WatchPbLong 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 |