org.sat4j.pb.constraints.pb
Class WatchPb

java.lang.Object
  org.sat4j.pb.constraints.pb.WatchPb

All Implemented Interfaces:

java.io.Serializable, org.sat4j.minisat.core.Constr, org.sat4j.minisat.core.Propagatable, org.sat4j.minisat.core.Undoable, PBConstr, org.sat4j.specs.IConstr

Direct Known Subclasses:

MaxWatchPb, MinWatchPb

public abstract class WatchPb
extends java.lang.Object
implements PBConstr, org.sat4j.minisat.core.Undoable, java.io.Serializable

See Also:

Serialized Form

Field Summary

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

Method Summary

void	assertConstraint(org.sat4j.minisat.core.UnitPropagationListener s)
void	calcReason(int p, org.sat4j.specs.IVecInt outReason) compute the reason for the assignment of a literal
boolean	coefficientsEqualToOne()
org.sat4j.specs.IVecInt	computeAnImpliedClause() compute an implied clause on the literals with the greater coefficients
boolean	equals(java.lang.Object pb)
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()
org.sat4j.minisat.core.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
boolean	learnt() is the constraint a learnt constrainte ?
boolean	locked() The constraint is the reason of a unit propagation.
static IDataStructurePB	niceCheckedParameters(org.sat4j.specs.IVecInt ps, org.sat4j.specs.IVec<java.math.BigInteger> bigCoefs, boolean moreThan, java.math.BigInteger bigDeg, org.sat4j.minisat.core.ILits voc)
static java.math.BigInteger	niceCheckedParametersForCompetition(int[] lits, java.math.BigInteger[] bc, boolean moreThan, java.math.BigInteger bigDeg)
static IDataStructurePB	niceParameters(org.sat4j.specs.IVecInt ps, org.sat4j.specs.IVec<java.math.BigInteger> bigCoefs, boolean moreThan, java.math.BigInteger bigDeg, org.sat4j.minisat.core.ILits voc)
static java.math.BigInteger	niceParametersForCompetition(int[] ps, java.math.BigInteger[] bigCoefs, boolean moreThan, java.math.BigInteger bigDeg)
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()
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
static java.math.BigInteger	toBigInt(int i)
java.lang.String	toString()
static org.sat4j.specs.IVec<java.math.BigInteger>	toVecBigInt(org.sat4j.specs.IVecInt vec)

Methods inherited from class java.lang.Object

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

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

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,
                       org.sat4j.specs.IVecInt outReason)

compute the reason for the assignment of a literal

Specified by:

calcReason in interface org.sat4j.minisat.core.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)

get

public int get(int i)

to obtain the i-th literal of the constraint

Specified by:

get in interface org.sat4j.specs.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 org.sat4j.minisat.core.Constr

Returns:

activity value of the constraint

See Also:

Constr.getActivity()

niceParameters

public static IDataStructurePB niceParameters(org.sat4j.specs.IVecInt ps,
                                              org.sat4j.specs.IVec<java.math.BigInteger> bigCoefs,
                                              boolean moreThan,
                                              java.math.BigInteger bigDeg,
                                              org.sat4j.minisat.core.ILits voc)
                                       throws org.sat4j.specs.ContradictionException

Throws:

org.sat4j.specs.ContradictionException

niceCheckedParameters

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

niceParametersForCompetition

public static java.math.BigInteger niceParametersForCompetition(int[] ps,
                                                                java.math.BigInteger[] bigCoefs,
                                                                boolean moreThan,
                                                                java.math.BigInteger bigDeg)
                                                         throws org.sat4j.specs.ContradictionException

Throws:

org.sat4j.specs.ContradictionException

niceCheckedParametersForCompetition

public static java.math.BigInteger niceCheckedParametersForCompetition(int[] lits,
                                                                       java.math.BigInteger[] bc,
                                                                       boolean moreThan,
                                                                       java.math.BigInteger bigDeg)

incActivity

public void incActivity(double claInc)

increase activity value of the constraint

Specified by:

incActivity in interface org.sat4j.minisat.core.Constr

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

learnt

public boolean learnt()

is the constraint a learnt constrainte ?

Specified by:

learnt in interface org.sat4j.specs.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 org.sat4j.minisat.core.Constr

Returns:

true

rescaleBy

public void rescaleBy(double d)

Permet le r??????chantillonage de l'activit??? de la contrainte

Specified by:

rescaleBy in interface org.sat4j.minisat.core.Constr

Parameters:

d - facteur d'ajustement

setLearnt

public void setLearnt()

La contrainte est apprise

Specified by:

setLearnt in interface org.sat4j.minisat.core.Constr

simplify

public boolean simplify()

Simplifie la contrainte(l'all???ge)

Specified by:

simplify in interface org.sat4j.minisat.core.Constr

Returns:

true si la contrainte est satisfaite, false sinon

size

public int size()

Specified by:

size in interface org.sat4j.specs.IConstr

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

assertConstraint

public void assertConstraint(org.sat4j.minisat.core.UnitPropagationListener s)

Specified by:

assertConstraint in interface org.sat4j.minisat.core.Constr

getDegree

public java.math.BigInteger getDegree()

Specified by:

getDegree in interface PBConstr

Returns:

Returns the degree.

register

public void register()

Specified by:

register in interface org.sat4j.minisat.core.Constr

toVecBigInt

public static org.sat4j.specs.IVec<java.math.BigInteger> toVecBigInt(org.sat4j.specs.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 org.sat4j.minisat.core.ILits getVocabulary()

Specified by:

getVocabulary in interface PBConstr

computeAnImpliedClause

public org.sat4j.specs.IVecInt computeAnImpliedClause()

compute an implied clause on the literals with the greater coefficients

Specified by:

computeAnImpliedClause in interface PBConstr

coefficientsEqualToOne

public boolean coefficientsEqualToOne()

equals

public boolean equals(java.lang.Object pb)

Overrides:

equals in class java.lang.Object

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object