public final class MaxWatchPb extends WatchPb
Modifier and Type | Field and Description |
---|---|
static int |
LIMIT_FOR_MAP |
Modifier and Type | Method and Description |
---|---|
protected void |
computePropagation(UnitPropagationListener s) |
protected void |
computeWatches()
All the literals are watched.
|
static MaxWatchPb |
normalizedMaxWatchPbNew(UnitPropagationListener s,
ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs)
build a pseudo boolean constraint.
|
static WatchPb |
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
|
assertConstraint, assertConstraintIfNeeded, calcReason, calcReasonOnTheFly, canBePropagatedMultipleTimes, coefficientsEqualToOne, computeAnImpliedClause, computeLeftSide, computeLeftSide, equals, forwardActivity, get, getActivity, getCoef, getCoefs, getDegree, getLits, getVocabulary, hashCode, incActivity, isAssertive, isSatisfiable, learnt, locked, ppcm, register, rescaleBy, setActivity, setLearnt, simplify, size, slackConstraint, slackConstraint, sort, sort, toConstraint, toString
public static final int LIMIT_FOR_MAP
protected void computeWatches() throws ContradictionException
computeWatches
in class WatchPb
ContradictionException
WatchPb.computeWatches()
protected void computePropagation(UnitPropagationListener s) throws ContradictionException
computePropagation
in class WatchPb
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 MaxWatchPb 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 constraintContradictionException
public static WatchPb 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.Copyright © 2013 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.