org.sat4j.specs

Interface IConstr

All Known Subinterfaces:

Constr, IWatchPb, PBConstr

All Known Implementing Classes:

AtLeast, AtLeastPB, BinaryClause, ConstrGroup, HTClause, LearntBinaryClause, LearntBinaryClausePB, LearntHTClause, LearntHTClausePB, LearntWLClause, MaxWatchCard, MaxWatchPb, MaxWatchPbLong, MaxWatchPbLongCP, MinWatchCard, MinWatchCardPB, MinWatchPb, MinWatchPbLong, MinWatchPbLongCP, OriginalBinaryClause, OriginalBinaryClausePB, OriginalHTClause, OriginalHTClausePB, OriginalWLClause, PuebloMinWatchPb, UnitClause, UnitClausePB, UnitClauses, UnitClausesPB, UnitWeightedClause, WatchPb, WatchPbLong, WatchPbLongCP, WLClause

public interface IConstr

The most general abstraction for handling a constraint.

Author:

leberre

Method Summary

Methods

Modifier and Type	Method and Description
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.
int	get(int i) returns the ith literal in the constraint
double	getActivity() To obtain the activity of the constraint.
boolean	learnt()
int	size()

Method Detail

learnt

boolean learnt()

Returns:

true iff the clause was learnt during the search

size

int size()

Returns:

the number of literals in the constraint.

get

int get(int i)

returns the ith literal in the constraint

Parameters:

i - the index of the literal

Returns:

a literal

getActivity

double getActivity()

To obtain the activity of the constraint.

Returns:

the activity of the clause.

Since:

2.1

canBePropagatedMultipleTimes

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. cardinality constraints and pseudo-boolean constraints).

Returns:

true if the constraint can be used several times as a reason to propagate a literal.

Since:

2.3.1