Package eu.bandm.tools.dpll

Class Clause<P>

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

Literals are accessible via the unmodifiable collection interface.

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

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

  • Method Details

    • isUnit

      public abstract boolean isUnit()
      Checks whether this clause is unitary.
      Returns:
      true if this clause contains exactly one literal; false otherwise.
      See Also:

    • getUnit

      @Opt public abstract @Opt Literal<P> getUnit()
      Extract the unit literal if appropriate.
      Returns:
      if this clause contains exactly one literal, it is returned; null otherwise.
      See Also:

    • score

      public int score()
      Returns a nonnegative measure of the syntactic complexity of this proposition.

      This implementation returns the sum of the scores of contained literals.

      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 some literal is 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.

    • given

      public abstract Clause<P> given(Literal<P> literal)
      Returns a simplified clause that is equivalent to this clause assuming the given literal.
      Parameters:
      literal - a literal to assume
      Returns:
      a simplified clause that is equivalent to this clause assuming the given literal
      Throws:
      NullPointerException - if literal is null

    • unit

      public static <P> Clause<P> unit(Literal<P> literal)
      Returns a unitary clause containing the given literal.
      Type Parameters:
      P - the type of propositional variables
      Parameters:
      literal - the literal
      Returns:
      a clause containing just literal
      Throws:
      NullPointerException - if literal is null

    • of

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

    • of

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

    • empty

      public static <P> Clause<P> empty()
      Returns an empty clause.

      The empty clause is unsatisfiable.

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

    • top

      public static <P> Clause<P> top()
      Returns a top clause.

      The top clause is always and evidently true.

      Type Parameters:
      P - the type of propositional variables
      Returns:
      a top clause
      See Also:

    • horn

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

      A Horn clause 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 clause
      Throws:
      NullPointerException - if consequent, antecedents or any element of antecedents is null

    • horn

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

      A Horn clause 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 clause
      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