org.sat4j.minisat.constraints.pb
Class WatchPb

java.lang.Object
  extended by org.sat4j.minisat.constraints.pb.WatchPb
All Implemented Interfaces:
java.io.Serializable, PBConstr, Constr, Propagatable, Undoable, IConstr
Direct Known Subclasses:
MaxWatchPb, MinWatchPb

public abstract class WatchPb
extends java.lang.Object
implements PBConstr, Undoable, java.io.Serializable

See Also:
Serialized Form

Field Summary
protected  double activity
          constraint activity
static boolean ATLEAST
          constant for the initial type of inequality more than or equal
static boolean ATMOST
          constant for the initial type of inequality less than or equal
protected  java.math.BigInteger[] coefs
          coefficients of the literals of the constraint
protected  java.math.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  boolean locked
          true if the constraint is the origin of unit propagation
protected  ILits voc
          constraint's vocabulary
protected  java.math.BigInteger watchCumul
          sum of the coefficients of the literals satisfied or unvalued
 
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 coefficientsEqualToOne()
           
 IVecInt computeAnImpliedClause()
          compute an implied clause on the literals with the greater coefficients
protected abstract  void computePropagation(UnitPropagationListener s)
           
protected abstract  void computeWatches()
           
 int get(int i)
          to obtain the i-th literal of the constraint
 double getActivity()
          to obtain the activity value of the constraint
 java.math.BigInteger getCoef(int i)
          to obtain the coefficient of the i-th literal of the constraint
 java.math.BigInteger[] getCoefs()
           
 java.math.BigInteger getDegree()
           
 int[] getLits()
           
 ILits getVocabulary()
           
 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()
          D?
 boolean learnt()
          is the constraint a learnt constrainte ?
 boolean locked()
          The constraint is the reason of a unit propagation.
static IDataStructurePB niceCheckedParameters(IVecInt ps, IVec<java.math.BigInteger> bigCoefs, boolean moreThan, java.math.BigInteger bigDeg, ILits voc)
           
static IDataStructurePB niceParameters(IVecInt ps, IVec<java.math.BigInteger> bigCoefs, boolean moreThan, java.math.BigInteger bigDeg, ILits voc)
           
protected static java.math.BigInteger ppcm(java.math.BigInteger a, java.math.BigInteger b)
          Calcule le ppcm de deux nombres
 java.math.BigInteger recalcLeftSide()
          compute the sum of the coefficients of the satisfied or non-assigned literals of the current constraint (usually called poss)
 java.math.BigInteger recalcLeftSide(java.math.BigInteger[] coefs)
          compute the sum of the coefficients of the satisfied or non-assigned literals of a described constraint (usually called poss)
 void register()
          Register the constraint to the solver.
 void rescaleBy(double d)
          Permet le r??????
 void setLearnt()
          La contrainte est apprise
 boolean simplify()
          Simplifie la contrainte(l'all???
 int size()
           
 java.math.BigInteger slackConstraint()
          compute the slack of the current constraint slack = poss - degree of the constraint
 java.math.BigInteger slackConstraint(java.math.BigInteger[] coefs, java.math.BigInteger degree)
          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 java.math.BigInteger toBigInt(int i)
           
 java.lang.String toString()
           
static IVec<java.math.BigInteger> toVecBigInt(IVecInt vec)
           
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, 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

ATMOST

public static final boolean ATMOST
constant for the initial type of inequality less than or equal

See Also:
Constant Field Values

ATLEAST

public static final boolean ATLEAST
constant for the initial type of inequality more than or equal

See Also:
Constant Field Values

activity

protected double activity
constraint activity


coefs

protected java.math.BigInteger[] coefs
coefficients of the literals of the constraint


degree

protected java.math.BigInteger 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


locked

protected boolean locked
true if the constraint is the origin of unit propagation


watchCumul

protected java.math.BigInteger watchCumul
sum of the coefficients of the literals satisfied or unvalued


voc

protected ILits voc
constraint's vocabulary

Method Detail

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

getCoef

public java.math.BigInteger getCoef(int i)
to obtain the coefficient of the i-th literal of the constraint

Specified by:
getCoef in interface PBConstr
Parameters:
i - index of the literal
Returns:
coefficient of the literal

getActivity

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

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

niceParameters

public static IDataStructurePB niceParameters(IVecInt ps,
                                              IVec<java.math.BigInteger> bigCoefs,
                                              boolean moreThan,
                                              java.math.BigInteger bigDeg,
                                              ILits voc)
                                       throws ContradictionException
Throws:
ContradictionException

niceCheckedParameters

public static IDataStructurePB niceCheckedParameters(IVecInt ps,
                                                     IVec<java.math.BigInteger> bigCoefs,
                                                     boolean moreThan,
                                                     java.math.BigInteger bigDeg,
                                                     ILits voc)

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 java.math.BigInteger slackConstraint()
compute the slack of the current constraint slack = poss - degree of the constraint

Returns:
la marge

slackConstraint

public java.math.BigInteger slackConstraint(java.math.BigInteger[] coefs,
                                            java.math.BigInteger degree)
compute the slack of a described constraint slack = poss - degree of the constraint

Parameters:
coefs - coefficients of the constraint
degree - degree of the constraint
Returns:
slack of the constraint

recalcLeftSide

public java.math.BigInteger recalcLeftSide(java.math.BigInteger[] coefs)
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

recalcLeftSide

public java.math.BigInteger recalcLeftSide()
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()
D?termine si la contrainte est toujours satisfiable

Returns:
la contrainte est encore satisfiable

learnt

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

Specified by:
learnt in interface IConstr
Returns:
true si la contrainte est apprise, false sinon
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 java.math.BigInteger ppcm(java.math.BigInteger a,
                                           java.math.BigInteger b)
Calcule le ppcm de deux nombres

Parameters:
a - premier nombre de l'op?ration
b - second nombre de l'op?ration
Returns:
le ppcm en question

rescaleBy

public void rescaleBy(double d)
Permet le r??????chantillonage de l'activit??? de la contrainte

Specified by:
rescaleBy in interface Constr
Parameters:
d - facteur d'ajustement

setLearnt

public void setLearnt()
La contrainte est apprise

Specified by:
setLearnt in interface Constr

simplify

public boolean simplify()
Simplifie la contrainte(l'all???ge)

Specified by:
simplify in interface Constr
Returns:
true si la contrainte est satisfaite, false sinon

size

public 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 java.lang.String toString()
Overrides:
toString in class java.lang.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.

getDegree

public java.math.BigInteger getDegree()
Specified by:
getDegree in interface PBConstr
Returns:
Returns the degree.

register

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

Specified by:
register in interface Constr

toVecBigInt

public static IVec<java.math.BigInteger> toVecBigInt(IVecInt vec)

toBigInt

public static java.math.BigInteger toBigInt(int i)

getCoefs

public java.math.BigInteger[] getCoefs()
Specified by:
getCoefs in interface PBConstr

getLits

public int[] getLits()
Specified by:
getLits in interface PBConstr

getVocabulary

public ILits getVocabulary()
Specified by:
getVocabulary in interface PBConstr

computeAnImpliedClause

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

Specified by:
computeAnImpliedClause in interface PBConstr

coefficientsEqualToOne

public boolean coefficientsEqualToOne()


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