Package eu.bandm.tools.dpll

Class SAT.Form<P>

java.lang.Object
java.util.AbstractCollection<SAT.Clause<P>>
eu.bandm.tools.dpll.SAT.Form<P>
All Implemented Interfaces:
Iterable<SAT.Clause<P>>, Collection<SAT.Clause<P>>
Enclosing class:
SAT<P>
protected abstract static class SAT.Form<P> extends AbstractCollection<SAT.Clause<P>>
Conjunction of clauses.

Clauses are accessible via the unmodifiable collection interface.

  • Constructor Details

    • Form

      protected Form()

  • Method Details

    • isTrue

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

    • isFalse

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

    • literals

      public abstract Iterable<SAT.Literal<? extends 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()

    • units

      abstract Iterable<SAT.Clause<P>> units()

    • pure

      abstract Set<SAT.Literal<? extends P>> pure()

    • propagate

      abstract SAT.Form<P> propagate(SAT.Literal<? extends P> lit)

    • nextUnit

      @Opt abstract @Opt eu.bandm.tools.dpll.SAT.Form.And<P> nextUnit()

    • and

      static <P> SAT.Form<P> and(SAT.Literal<? extends P> first, SAT.Form<P> rest)

    • and

      static <P> SAT.Form<P> and(SAT.Clause<P> first, SAT.Form<P> rest)

    • and

      @SafeVarargs static <P> SAT.Form<P> and(SAT.Clause<P>... cs)

    • and

      static <P> SAT.Form<P> and(Collection<? extends SAT.Clause<P>> cs)