Class SAT.Clause<P>

java.lang.Object
java.util.AbstractCollection<SAT.Literal<? extends P>>
eu.bandm.tools.util.SAT.Clause<P>
All Implemented Interfaces:
Iterable<SAT.Literal<? extends P>>, Collection<SAT.Literal<? extends P>>
Enclosing class:
SAT<P>

protected abstract static class SAT.Clause<P> extends AbstractCollection<SAT.Literal<? extends P>>
Disjunction of literals.

Literals are accessible via the unmodifiable collection interface.

  • Constructor Details

    • Clause

      protected Clause()
  • Method Details

    • isTrue

      public abstract boolean isTrue()
      Check whether this clause is tautological.
      Returns:
      true if this clause is true under all interpretations; false otherwise.
    • isFalse

      public abstract boolean isFalse()
      Check whether this clause is unsatisfiable.
      Returns:
      true if this clause is false under all interpretations; false otherwise.
    • isUnit

      public abstract boolean isUnit()
      Check whether this clause is unitary.
      Returns:
      true if this clause contains exactly one literal; false otherwise.
    • getUnit

      public abstract SAT.Literal<? extends P> getUnit()
      Extract unit literal.
      Returns:
      if this clause contains exactly one literal, it is returned; null otherwise.
    • score

      public int score()
    • propagate

      abstract SAT.Clause<P> propagate(SAT.Literal<? extends P> lit)
    • or

      static <P> SAT.Clause<P> or(SAT.Literal<? extends P> first, SAT.Clause<P> rest)
    • or

      @SafeVarargs static <P> SAT.Clause<P> or(SAT.Literal<? extends P>... lits)