|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object org.sat4j.pb.constraints.pb.WatchPb
public abstract class WatchPb
Abstract data structure for pseudo-boolean constraint with watched literals.
Field Summary | |
---|---|
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 |
Method Summary | |
---|---|
void |
assertConstraint(UnitPropagationListener s)
|
void |
calcReason(int p,
IVecInt outReason)
compute the reason for the assignment of a literal |
boolean |
canBePropagatedMultipleTimes()
|
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()
|
void |
rescaleBy(double d)
to re-scale the activity of the constraint |
void |
setActivity(double d)
|
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()
|
String |
toString()
|
Methods inherited from class java.lang.Object |
---|
clone, finalize, getClass, notify, notifyAll, wait, wait, wait |
Methods inherited from interface org.sat4j.minisat.core.Constr |
---|
remove |
Methods inherited from interface org.sat4j.minisat.core.Propagatable |
---|
propagate |
Methods inherited from interface org.sat4j.minisat.core.Undoable |
---|
undo |
Field Detail |
---|
protected double activity
protected BigInteger[] coefs
protected BigInteger sumcoefs
protected BigInteger degree
protected int[] lits
protected boolean learnt
protected ILits voc
Method Detail |
---|
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)
get
in interface IConstr
i
- index of the literal
public BigInteger getCoef(int i)
getCoef
in interface PBConstr
i
- index of the literal
public double getActivity()
getActivity
in interface IConstr
IConstr.getActivity()
public void incActivity(double claInc)
incActivity
in interface Constr
Constr.incActivity(double)
public void setActivity(double d)
setActivity
in interface Constr
public BigInteger slackConstraint()
public BigInteger slackConstraint(BigInteger[] theCoefs, BigInteger theDegree)
slackConstraint
in interface IWatchPb
theCoefs
- coefficients of the constrainttheDegree
- degree of the constraint
public BigInteger computeLeftSide(BigInteger[] theCoefs)
coefs
- coefficients of the constraint
public BigInteger computeLeftSide()
protected boolean isSatisfiable()
public boolean learnt()
learnt
in interface IConstr
IConstr.learnt()
public boolean locked()
locked
in interface Constr
protected static BigInteger ppcm(BigInteger a, BigInteger b)
a
- one integerb
- the other integer
public void rescaleBy(double d)
rescaleBy
in interface Constr
d
- adjusting factorpublic void setLearnt()
setLearnt
in interface Constr
public boolean simplify()
simplify
in interface Constr
public final int size()
size
in interface IConstr
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 String toString()
toString
in class Object
public void assertConstraint(UnitPropagationListener s)
assertConstraint
in interface Constr
public BigInteger getDegree()
getDegree
in interface PBConstr
public void register()
register
in interface Constr
public BigInteger[] getCoefs()
getCoefs
in interface PBConstr
public int[] getLits()
getLits
in interface PBConstr
public ILits getVocabulary()
getVocabulary
in interface PBConstr
public IVecInt computeAnImpliedClause()
computeAnImpliedClause
in interface PBConstr
public boolean coefficientsEqualToOne()
public boolean equals(Object pb)
equals
in class Object
public int hashCode()
hashCode
in class Object
public void forwardActivity(double claInc)
forwardActivity
in interface Constr
public boolean canBePropagatedMultipleTimes()
canBePropagatedMultipleTimes
in interface IConstr
public Constr toConstraint()
toConstraint
in interface Propagatable
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |