Package eu.bandm.tools.dpll

Class Formula<P>

java.lang.Object
java.util.AbstractCollection<Clause<P>>
eu.bandm.tools.dpll.Formula<P>
Type Parameters:
P - the type of propositional variables
All Implemented Interfaces:
Proposition<P>, Iterable<Clause<P>>, Collection<Clause<P>>
public abstract class Formula<P> extends AbstractCollection<Clause<P>> implements Proposition<P>
Conjunction of clauses.

Clauses are accessible via the unmodifiable collection interface.

All instances of this class are created via static factory methods.

Although conjunction is commutative and idempotent, and hence the semantics of a formula is determined by the set of contained clauses, this class uses a purely syntactic list representation where the order and duplicity of given clauses are preserved. Hence the representational equality of two formulas is not a useful semantical property. In particular, it is insufficient for determining logical equivalence, and collecting formulas in a set does not prevent redundancy.

  • Method Details

    • literals

      public abstract Iterable<Literal<P>> literals()
      View literals occurring in this formula.
      Returns:
      an unmodifiable enumeration of literals in all clauses of this formula, in textual order and with duplicates.

    • score

      public int score()
      Returns a nonnegative measure of the syntactic complexity of this proposition.
      Specified by:
      score in interface Proposition<P>
      Returns:
      the number of literal occurrences in this proposition

    • isSatisfiedBy

      public boolean isSatisfiedBy(Set<Literal<P>> solution)
      Checks whether this proposition is satisfied by a given solution.

      This implementation returns true if all clauses are satisfied.

      Specified by:
      isSatisfiedBy in interface Proposition<P>
      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

      public 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.

      This implementation returns true if all clauses are disjunction free.

      Specified by:
      isDisjunctionFree in interface Proposition<P>
      Returns:
      true if this proposition is free of disjunctions

    • units

      public abstract Iterable<Clause<P>> units()
      Enumerates all unit clauses in this formula.
      Returns:
      an enumeration of all unit clauses in this formula in textual order.
      See Also:

    • pure

      abstract Set<Literal<P>> pure()
      Returns the set of all literals occuring purely in this formula.

      A literal occurs purely if it occurs, but its negation does not.

      This operation is expensive and should not be invoked too often.

      Returns:
      the set of all literals occuring purely in this formula

    • given

      public abstract Formula<P> given(Literal<P> literal)
      Returns a formula that abstracts from the given literal in this formula.

      The resulting formula does not contain the given literal or its negation. It is satsified by exactly the same consistent solutions that contain the given literal as this formula.

      Parameters:
      literal - the literal to abstract from
      Returns:
      a formula that abstracts from the given literal in this formula
      Throws:
      NullPointerException - if literal is null

    • empty

      public static <P> Formula<P> empty()
      Returns an empty formula.

      The empty formula is evidently true.

      Type Parameters:
      P - the type of propositional variables
      Returns:
      an empty formula
      See Also:

    • bottom

      public static <P> Formula<P> bottom()
      Returns a bottom formula.

      The bottom formula is evidently false.

      Type Parameters:
      P - the type of propositional variables
      Returns:
      a bottom formula
      See Also:

    • with

      public Formula<P> with(Literal<P> first)
      Returns a formula that prepends a unit clause to this formula.
      Parameters:
      first - the literal of the unit clause to prepend
      Returns:
      a formula that has a unit clause with the given literal before all clauses of this formula
      Throws:
      NullPointerException - if first is null

    • with

      public Formula<P> with(Clause<P> first)
      Returns a formula that prepends a clause to this formula.
      Parameters:
      first - the clause to prepend
      Returns:
      a formula that has the given clause before all clauses of this formula
      Throws:
      NullPointerException - if first is null

    • and

      public Formula<P> and(Formula<P> other)
      Returns the conjunction of this and another formula.

      The clauses of both parts are concatenated; there is no attempt to detect duplicates.

      Parameters:
      other - the other formula
      Returns:
      the conjunction of this and other
      Throws:
      NullPointerException - if other is null

    • of

      @SafeVarargs public static <P> Formula<P> of(Clause<P>... clauses)
      Returns a formula containing the given clauses.
      Type Parameters:
      P - the type of propositional variables
      Parameters:
      clauses - some clauses
      Returns:
      a formula contains the given clauses in order
      Throws:
      NullPointerException - if clauses is null or contains a null element

    • of

      public static <P> Formula<P> of(List<? extends Clause<P>> clauses)
      Returns a formula containing the given clauses.
      Type Parameters:
      P - the type of propositional variables
      Parameters:
      clauses - some clauses
      Returns:
      a formula contains the given clauses in order
      Throws:
      NullPointerException - if clauses is null or contains a null element

    • horn

      @SafeVarargs public static <P> Formula<P> horn(P consequent, P... antecedents)
      Returns a Horn formula with the given consequent and antecedents.

      A Horn formula contains a single clause that has exactly one positive literal, the consequent; all negative literals are antecedents.

      Type Parameters:
      P - the type of propositional variables
      Parameters:
      consequent - the propositional variable of the consequent
      antecedents - the propositional variables of the antecedents
      Returns:
      a Horn formula
      Throws:
      NullPointerException - if consequent, antecedents or any element of antecedents is null

    • horn

      public static <P> Formula<P> horn(P consequent, Collection<? extends P> antecedents)
      Returns a Horn formula with the given consequent and antecedents.

      A Horn formula contains a single clause that has exactly one positive literal, the consequent; all negative literals are antecedents.

      Type Parameters:
      P - the type of propositional variables
      Parameters:
      consequent - the propositional variable of the consequent
      antecedents - the propositional variables of the antecedents
      Returns:
      a Horn formula
      Throws:
      NullPointerException - if consequent, antecedents or any element of antecedents is null

    • equals

      public boolean equals(Object o)
      Specified by:
      equals in interface Collection<P>
      Overrides:
      equals in class Object