public abstract class WatchPb extends Object implements IWatchPb, Propagatable, Undoable, Serializable
Modifier and Type | Field and Description |
---|---|
protected double |
activity
constraint activity
|
protected BigInteger[] |
coefs
coefficients of the literals of the constraint
|
protected BigInteger |
degree
degree of the pseudo-boolean constraint
|
protected boolean |
learnt
true if the constraint is a learned constraint
|
protected int[] |
lits
literals of the constraint
|
protected BigInteger |
sumcoefs |
protected ILits |
voc
constraint's vocabulary
|
Modifier and Type | Method and Description |
---|---|
void |
assertConstraint(UnitPropagationListener s)
Method called when the constraint is to be asserted.
|
void |
assertConstraintIfNeeded(UnitPropagationListener s)
Method called when the constraint is added to the solver "on the fly".
|
void |
calcReason(int p,
IVecInt outReason)
compute the reason for the assignment of a literal
|
void |
calcReasonOnTheFly(int p,
IVecInt trail,
IVecInt outReason)
Compute the reason for a given assignment in a the constraint created on
the fly in the solver.
|
boolean |
canBePropagatedMultipleTimes()
Partition constraints into the ones that can only be found once on the
trail (e.g. clauses) and the ones that can be found several times (e.g.
|
boolean |
coefficientsEqualToOne() |
IVecInt |
computeAnImpliedClause()
compute an implied clause on the literals with the greater coefficients.
|
BigInteger |
computeLeftSide()
compute the sum of the coefficients of the satisfied or non-assigned
literals of the current constraint (usually called poss)
|
BigInteger |
computeLeftSide(BigInteger[] theCoefs)
compute the sum of the coefficients of the satisfied or non-assigned
literals of a described constraint (usually called poss)
|
protected abstract void |
computePropagation(UnitPropagationListener s) |
protected abstract void |
computeWatches() |
boolean |
equals(Object pb) |
void |
forwardActivity(double claInc) |
int |
get(int i)
to obtain the i-th literal of the constraint
|
double |
getActivity()
to obtain the activity value of the constraint
|
BigInteger |
getCoef(int i)
to obtain the coefficient of the i-th literal of the constraint
|
BigInteger[] |
getCoefs()
to obtain the coefficients of the constraint.
|
BigInteger |
getDegree() |
int[] |
getLits()
to obtain the literals of the constraint.
|
ILits |
getVocabulary() |
int |
hashCode() |
void |
incActivity(double claInc)
increase activity value of the constraint
|
boolean |
isAssertive(int dl)
This predicate tests wether the constraint is assertive at decision level
dl
|
protected boolean |
isSatisfiable()
tests if the constraint is still satisfiable.
|
boolean |
learnt()
is the constraint a learnt constraint ?
|
boolean |
locked()
The constraint is the reason of a unit propagation.
|
protected static BigInteger |
ppcm(BigInteger a,
BigInteger b)
ppcm : least common multiple for two integers (plus petit commun
multiple)
|
void |
register()
Register the constraint to the solver.
|
void |
rescaleBy(double d)
to re-scale the activity of the constraint
|
void |
setActivity(double d)
Set the activity at a specific value
|
void |
setLearnt()
the constraint is learnt
|
boolean |
simplify()
simplify the constraint (if it is satisfied)
|
int |
size() |
BigInteger |
slackConstraint()
compute the slack of the current constraint slack = poss - degree of the
constraint
|
BigInteger |
slackConstraint(BigInteger[] theCoefs,
BigInteger theDegree)
compute the slack of a described constraint slack = poss - degree of the
constraint
|
protected void |
sort()
sort coefficient and literal arrays
|
protected void |
sort(int from,
int to)
sort partially coefficient and literal arrays
|
Constr |
toConstraint()
Allow to access a constraint view of the propagatable to avoid casting.
|
String |
toString() |
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
propagate
protected double activity
protected BigInteger[] coefs
protected BigInteger sumcoefs
protected BigInteger degree
protected int[] lits
protected boolean learnt
protected ILits voc
public boolean isAssertive(int dl)
dl
- public void calcReason(int p, IVecInt outReason)
calcReason
in interface Constr
p
- a falsified literal (or Lit.UNDEFINED)outReason
- list of falsified literals for which the negation is the
reason of the assignmentConstr.calcReason(int, IVecInt)
protected abstract void computeWatches() throws ContradictionException
ContradictionException
protected abstract void computePropagation(UnitPropagationListener s) throws ContradictionException
ContradictionException
public int get(int i)
public BigInteger getCoef(int i)
public double getActivity()
getActivity
in interface IConstr
IConstr.getActivity()
public void incActivity(double claInc)
incActivity
in interface Constr
claInc
- the value to increase the activity withConstr.incActivity(double)
public void setActivity(double d)
Constr
setActivity
in interface Constr
d
- the new activitypublic BigInteger slackConstraint()
public BigInteger slackConstraint(BigInteger[] theCoefs, BigInteger theDegree)
slackConstraint
in interface IWatchPb
theCoefs
- coefficients of the constrainttheDegree
- degree of the constraintpublic BigInteger computeLeftSide(BigInteger[] theCoefs)
coefs
- coefficients of the constraintpublic BigInteger computeLeftSide()
protected boolean isSatisfiable()
public boolean learnt()
learnt
in interface IConstr
IConstr.learnt()
public boolean locked()
protected static BigInteger ppcm(BigInteger a, BigInteger b)
a
- one integerb
- the other integerpublic void rescaleBy(double d)
public void setLearnt()
public boolean simplify()
public final int size()
protected final void sort()
protected final void sort(int from, int to)
from
- index for the beginning of the sortto
- index for the end of the sortpublic void assertConstraint(UnitPropagationListener s)
Constr
assertConstraint
in interface Constr
s
- a UnitPropagationListener to use for unit propagation.public void assertConstraintIfNeeded(UnitPropagationListener s)
Constr
Constr.assertConstraint(UnitPropagationListener)
method.assertConstraintIfNeeded
in interface Constr
s
- a UnitPropagationListener to use for unit propagation.public BigInteger getDegree()
public void register()
Constr
public BigInteger[] getCoefs()
public int[] getLits()
public ILits getVocabulary()
getVocabulary
in interface PBConstr
public IVecInt computeAnImpliedClause()
computeAnImpliedClause
in interface PBConstr
public boolean coefficientsEqualToOne()
public void forwardActivity(double claInc)
forwardActivity
in interface Constr
public boolean canBePropagatedMultipleTimes()
IConstr
canBePropagatedMultipleTimes
in interface IConstr
public Constr toConstraint()
Propagatable
toConstraint
in interface Propagatable
public void calcReasonOnTheFly(int p, IVecInt trail, IVecInt outReason)
Constr
Constr.calcReason(int, IVecInt)
, the falsification may not have been
detected as soon as possible. As such, it is necessary to take into
account the order of the literals in the trail.calcReasonOnTheFly
in interface Constr
p
- a satisfied literal (or Lit.UNDEFINED)trail
- all the literals satisfied in the solvers, should not be
modified.outReason
- a list of falsified literals whose negation is the reason of
the assignment of p to true.Copyright © 2013 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.