|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object org.sat4j.pb.constraints.pb.WatchPbLongCP org.sat4j.pb.constraints.pb.MaxWatchPbLongCP
public final class MaxWatchPbLongCP
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 |
---|
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 |
---|
protected void computeWatches() throws ContradictionException
computeWatches
in class WatchPbLongCP
ContradictionException
WatchPbLong.computeWatches()
protected void computePropagation(UnitPropagationListener s) throws ContradictionException
computePropagation
in class WatchPbLongCP
ContradictionException
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
- an unassigned literalpublic static MaxWatchPbLongCP normalizedMaxWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs) throws ContradictionException
s
- a unit propagation listener (usually the solver)voc
- the vocabularylits
- the literals of the constraintcoefs
- the coefficients of the constraintdegree
- the degree of the constraint
ContradictionException
public 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.
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |