org.sat4j.minisat.core
Interface Constr

All Superinterfaces:

IConstr, Propagatable

All Known Subinterfaces:

PBConstr

All Known Implementing Classes:

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

public interface Constr
extends Propagatable, IConstr

Basic constraint abstraction used in Solver. Any new constraint type should implement that interface.

Author:

leberre

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 a given assignment.
double	getActivity() To obtain the activity of the constraint.
void	incActivity(double claInc) Increase the constraint activity.
boolean	locked() Indicate wether a constraint is responsible from an assignment.
void	register() Register the constraint to the solver.
void	remove() Remove a constraint from the solver.
void	rescaleBy(double d) Rescale the clause activity by a value.
void	setLearnt() Mark a constraint as learnt.
boolean	simplify() Simplifies a constraint, by removing top level falsified literals for instance.

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()

Remove a constraint from the solver.

simplify

boolean simplify()

Simplifies a constraint, by removing top level falsified literals for instance.

Returns:

true iff the constraint is satisfied.

calcReason

void calcReason(int p,
                IVecInt outReason)

Compute the reason for a given assignment. If the constraint is a clause, it is supposed to be either a unit clause or a falsified one.

Parameters:

p - a satisfied literal (or Lit.UNDEFINED)

outReason - the list of falsified literals whose negation is the reason of the assignment of p to true.

incActivity

void incActivity(double claInc)

Increase the constraint activity.

Parameters:

claInc - the value to increase the activity with

getActivity

double getActivity()

To obtain the activity of the constraint.

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.