org.sat4j.pb.constraints.pb
Class WatchPbLong

java.lang.Object
  extended by org.sat4j.pb.constraints.pb.WatchPbLong
All Implemented Interfaces:
Serializable, Constr, Propagatable, Undoable, IConstr
Direct Known Subclasses:
MaxWatchPbLong, MinWatchPbLong, MinWatchPbLongLimit

public abstract class WatchPbLong
extends Object
implements Constr, Undoable, Serializable

See Also:
Serialized Form

Field Summary
protected  double activity
          constraint activity
protected  long[] coefs
          coefficients of the literals of the constraint
protected  long 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  ILits voc
          constraint's vocabulary
 
Method Summary
 void assertConstraint(UnitPropagationListener s)
          Method called when the constraint is to be asserted.
 void calcReason(int p, IVecInt outReason)
          compute the reason for the assignment of a literal
 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.
 long computeLeftSide()
          compute the sum of the coefficients of the satisfied or non-assigned literals of the current constraint (usually called poss)
 long computeLeftSide(long[] 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
 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)
 boolean propagate(UnitPropagationListener s, int p)
          Propagate the truth value of a literal in constraints in which that literal is falsified.
 void register()
          Register the constraint to the solver.
 void remove(UnitPropagationListener upl)
          Remove a constraint from the solver.
 void rescaleBy(double d)
          to re-scale the activity of the constraint
 void setLearnt()
          the constraint is learnt
 boolean simplify()
          simplify the constraint (if it is satisfied)
 int size()
           
 long slackConstraint()
          compute the slack of the current constraint slack = poss - degree of the constraint
 long slackConstraint(long[] theCoefs, long 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
static long[] toLong(BigInteger[] bigValues)
           
 String toString()
           
 void undo(int p)
          Method called when backtracking
 
Methods inherited from class java.lang.Object
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
 

Field Detail

activity

protected double activity
constraint activity


coefs

protected long[] coefs
coefficients of the literals of the constraint


degree

protected long degree
degree of the pseudo-boolean constraint


lits

protected int[] lits
literals of the constraint


learnt

protected boolean learnt
true if the constraint is a learned constraint


voc

protected ILits voc
constraint's vocabulary

Method Detail

toLong

public static long[] toLong(BigInteger[] bigValues)

isAssertive

public boolean isAssertive(int dl)
This predicate tests wether the constraint is assertive at decision level dl

Parameters:
dl -
Returns:
true iff the constraint is assertive at decision level dl.

calcReason

public void calcReason(int p,
                       IVecInt outReason)
compute the reason for the assignment of a literal

Specified by:
calcReason in interface Constr
Parameters:
p - a falsified literal (or Lit.UNDEFINED)
outReason - list of falsified literals for which the negation is the reason of the assignment
See Also:
Constr.calcReason(int, IVecInt)

computeWatches

protected abstract void computeWatches()
                                throws ContradictionException
Throws:
ContradictionException

computePropagation

protected abstract void computePropagation(UnitPropagationListener s)
                                    throws ContradictionException
Throws:
ContradictionException

get

public int get(int i)
to obtain the i-th literal of the constraint

Specified by:
get in interface IConstr
Parameters:
i - index of the literal
Returns:
the literal

getActivity

public double getActivity()
to obtain the activity value of the constraint

Specified by:
getActivity in interface IConstr
Returns:
activity value of the constraint
See Also:
IConstr.getActivity()

incActivity

public void incActivity(double claInc)
increase activity value of the constraint

Specified by:
incActivity in interface Constr
Parameters:
claInc - the value to increase the activity with
See Also:
Constr.incActivity(double)

slackConstraint

public long slackConstraint()
compute the slack of the current constraint slack = poss - degree of the constraint

Returns:
la marge

slackConstraint

public long slackConstraint(long[] theCoefs,
                            long theDegree)
compute the slack of a described constraint slack = poss - degree of the constraint

Parameters:
theCoefs - coefficients of the constraint
theDegree - degree of the constraint
Returns:
slack of the constraint

computeLeftSide

public long computeLeftSide(long[] theCoefs)
compute the sum of the coefficients of the satisfied or non-assigned literals of a described constraint (usually called poss)

Parameters:
coefs - coefficients of the constraint
Returns:
poss

computeLeftSide

public long computeLeftSide()
compute the sum of the coefficients of the satisfied or non-assigned literals of the current constraint (usually called poss)

Returns:
poss

isSatisfiable

protected boolean isSatisfiable()
tests if the constraint is still satisfiable. this method is only called in assertions.

Returns:
the constraint is satisfiable

learnt

public boolean learnt()
is the constraint a learnt constraint ?

Specified by:
learnt in interface IConstr
Returns:
true if the constraint is learnt, else false
See Also:
IConstr.learnt()

locked

public boolean locked()
The constraint is the reason of a unit propagation.

Specified by:
locked in interface Constr
Returns:
true

ppcm

protected static BigInteger ppcm(BigInteger a,
                                 BigInteger b)
ppcm : least common multiple for two integers (plus petit commun multiple)

Parameters:
a - one integer
b - the other integer
Returns:
the least common multiple of a and b

rescaleBy

public void rescaleBy(double d)
to re-scale the activity of the constraint

Specified by:
rescaleBy in interface Constr
Parameters:
d - adjusting factor

setLearnt

public void setLearnt()
the constraint is learnt

Specified by:
setLearnt in interface Constr

simplify

public boolean simplify()
simplify the constraint (if it is satisfied)

Specified by:
simplify in interface Constr
Returns:
true if the constraint is satisfied, else false

size

public final int size()
Specified by:
size in interface IConstr
Returns:
the number of literals in the constraint.

sort

protected final void sort()
sort coefficient and literal arrays


sort

protected final void sort(int from,
                          int to)
sort partially coefficient and literal arrays

Parameters:
from - index for the beginning of the sort
to - index for the end of the sort

toString

public String toString()
Overrides:
toString in class Object

assertConstraint

public void assertConstraint(UnitPropagationListener s)
Description copied from interface: Constr
Method called when the constraint is to be asserted. It means that the constraint was learnt during the search and it should now propagate some truth values. In the clausal case, only one literal should be propagated. In other cases, it might be different.

Specified by:
assertConstraint in interface Constr
Parameters:
s - a UnitPropagationListener to use for unit propagation.

register

public void register()
Description copied from interface: Constr
Register the constraint to the solver.

Specified by:
register in interface Constr

getLits

public int[] getLits()
to obtain the literals of the constraint.

Returns:
a copy of the array of the literals

getVocabulary

public ILits getVocabulary()

computeAnImpliedClause

public IVecInt computeAnImpliedClause()
compute an implied clause on the literals with the greater coefficients.

Returns:
a vector containing the literals for this clause.

coefficientsEqualToOne

public boolean coefficientsEqualToOne()

equals

public boolean equals(Object pb)
Overrides:
equals in class Object

hashCode

public int hashCode()
Overrides:
hashCode in class Object

forwardActivity

public void forwardActivity(double claInc)
Specified by:
forwardActivity in interface Constr

remove

public void remove(UnitPropagationListener upl)
Description copied from interface: Constr
Remove a constraint from the solver.

Specified by:
remove in interface Constr

propagate

public boolean propagate(UnitPropagationListener s,
                         int p)
Description copied from interface: Propagatable
Propagate the truth value of a literal in constraints in which that literal is falsified.

Specified by:
propagate in interface Propagatable
Parameters:
s - something able to perform unit propagation
p - the literal being propagated. Its negation must appear in the constraint.
Returns:
false iff an inconsistency (a contradiction) is detected.

undo

public void undo(int p)
Description copied from interface: Undoable
Method called when backtracking

Specified by:
undo in interface Undoable
Parameters:
p - a literal to be unassigned.

canBePropagatedMultipleTimes

public boolean canBePropagatedMultipleTimes()
Description copied from interface: IConstr
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. cardinality constraints and pseudo-boolean constraints).

Specified by:
canBePropagatedMultipleTimes in interface IConstr
Returns:
true if the constraint can be used several times as a reason to propagate a literal.


Copyright © 2011 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.