Package eu.bandm.tools.dpll

Interface Proposition<P>

Type Parameters:

P - the type of propositional variables

All Known Implementing Classes:

Clause, Formula, Literal

public interface Proposition<P>

A logical proposition.

Method Summary

Modifier and Type	Method	Description
boolean	isDisjunctionFree()	Checks whether this proposition is free of disjunctions.
boolean	isFalse()	Check whether this proposition is evidently false.
boolean	isSatisfiedBy(Set<Literal<P>> solution)	Checks whether this proposition is satisfied by a given solution.
boolean	isTrue()	Check whether this proposition is evidently true.
int	score()	Returns a nonnegative measure of the syntactic complexity of this proposition.

Method Details

isTrue

boolean isTrue()

Check whether this proposition is evidently true.

Returns:

true if this proposition is immediately seen to be true; false otherwise.

isFalse

boolean isFalse()

Check whether this proposition is evidently false.

Returns:

true if this proposition is immediately seen to be false; false otherwise.

score

int score()

Returns a nonnegative measure of the syntactic complexity of this proposition.

Returns:

the number of literal occurrences in this proposition

isSatisfiedBy

boolean isSatisfiedBy(Set<Literal<P>> solution)

Checks whether this proposition is satisfied by a given solution.

Parameters:

solution - the solution to check for satisfaction

Returns:

true if assuming that all literals in solution are true entails that this proposition is true; false otherwise.

isDisjunctionFree

boolean isDisjunctionFree()

Checks whether this proposition is free of disjunctions.

A disjunction-free proposition is satisfied by at most one solution that uses the same propositional variables.

Returns:

true if this proposition is free of disjunctions