org.sat4j.minisat.core
Interface Constr

All Superinterfaces:

IConstr, Propagatable

All Known Subinterfaces:

PBConstr

All Known Implementing Classes:

AtLeast, AtLeastPB, BinaryClauses, CBClause, MaxWatchCard, MaxWatchPb, MinWatchCard, MinWatchCardPB, MinWatchPb, MixableCBClause, MixableCBClausePB, PuebloMinWatchPb, TernaryClauses, WatchPb, WLClause, WLClausePB

public interface Constr
extends Propagatable, IConstr

Author:

leberre Cette interface repr?sente les services offerts par une contrainte

Method Summary

void	assertConstraint(UnitPropagationListener s) Method called when the constraint is to be asserted.
void	calcReason(int p, IVecInt outReason) Calcule la cause de l'affection d'un litt?
double	getActivity()
void	incActivity(double claInc)
boolean	locked() Indicate wether a constraint is responsible from an assignment.
void	register() Register the constraint to the solver.
void	remove() Enl?
void	rescaleBy(double d) Rescale the clause activity by a value.
void	setLearnt() Mark a constraint as learnt.
boolean	simplify() Simplifie une contrainte, par exemple en enlevant les litt?

Methods inherited from interface org.sat4j.minisat.core.Propagatable

propagate

Methods inherited from interface org.sat4j.specs.IConstr

get, learnt, size

Method Detail

remove

void remove()

Enl?ve une contrainte du prouveur

simplify

boolean simplify()

Simplifie une contrainte, par exemple en enlevant les litt?raux falsifi?s.

Returns:

true ssi la contrainte est satisfaite.

calcReason

void calcReason(int p,
                IVecInt outReason)

Calcule la cause de l'affection d'un litt?ral

Parameters:

p - un litt?ral falsifi? (ou Lit.UNDEFINED)

outReason - la liste des litt?raux falsifi?s dont la n?gation correspond ? la raison de l'affectation.

incActivity

void incActivity(double claInc)

Parameters:

claInc - the value to increase the activity with

getActivity

double getActivity()

Returns:

the activity of the clause.

locked

boolean locked()

Indicate wether a constraint is responsible from an assignment.

Returns:

true if a constraint is a "reason" for an assignment.

setLearnt

void setLearnt()

Mark a constraint as learnt.

register

void register()

Register the constraint to the solver.

rescaleBy

void rescaleBy(double d)

Rescale the clause activity by a value.

Parameters:

d - the value to rescale the clause activity with.

assertConstraint

void assertConstraint(UnitPropagationListener s)

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.

Parameters:

s - a UnitPropagationListener to use for unit propagation.