Chapter 18. Horn and 2-SAT Satisfiability

Polynomial-time fragments of SAT: forward chaining, lattice-linearity, and implication graphs.

This page: LLP forms. View classical forms »

Horn formulas

A Horn formula is a CNF where every clause has at most one positive literal. Each clause can be written as an implication $(x_{i_1} \wedge \cdots \wedge x_{i_k}) \to h$, where $h$ is a variable (a definite clause), a unit fact ($\top \to y$), or $\bot$ (a goal or negative clause). Horn formulas are central in logic programming and database theory.

The key structural property is the meet-closure: if $G$ and $H$ both satisfy a Horn formula, then so does $G \sqcap H$ (the componentwise AND). This means the set of satisfying assignments forms a lattice, and the least model (the smallest satisfying assignment) is unique and computable in linear time.

2-SAT formulas

A 2-SAT formula is a CNF where every clause has exactly two literals. Unlike 3-SAT (which is NP-complete), 2-SAT is solvable in linear time via the implication graph: each clause $(a \lor b)$ generates two implications $(\lnot a \to b)$ and $(\lnot b \to a)$. The formula is satisfiable iff no variable and its negation belong to the same strongly connected component.

LLP-HornSAT

The LLP form. The forbidden predicate detects a variable $x_j$ that is false but implied by a clause whose antecedents are all true. Advancing sets $G[j] := \mathrm{true}$. The fixed point is the least model. The meet-closure property of Horn formulas guarantees lattice-linearity.

Time complexity: $O(n + m)$, where $n$ is the number of variables and $m$ is the total clause length.

boolean[] LLPHornSAT(int[][] body, int[] head) {
  int n = head.length;
  boolean[] G = new boolean[n];
  forbidden (j) : hornImplied(j, G, body, head) =>
    advance : G[j] = true;
  return G;
}

LLP-QHornSAT

Solve a q-Horn formula by composing HornSAT on $X$ variables with 2-SAT on $Y$ variables. This is a composite algorithm with two phases.

// LLP-QHornSAT: solve q-horn formula by composing HornSAT on X
// variables with 2-SAT on Y variables.
// This is a composite algorithm, not a single forbidden/advance pair.

class LLPQHornSAT {
  boolean[] LLPQHornSAT(int[][] body1, int[] head1, int[][] clauses2, int n1, int n2) {
    boolean[] G = new boolean[n1];
    boolean[] H = new boolean[n2];
    // Phase 1: solve Horn clauses on X variables
    int j = 0;
    while (j < n1) {
      G[j] = false;
      j = j + 1;
    };
    forbidden (j) : hornImplied(j, G, body1, head1) =>
      advance : G[j] = true;
    // Phase 2: substitute X values into Type-2 clauses, solve 2-SAT on Y
    j = 0;
    while (j < n2) {
      H[j] = false;
      j = j + 1;
    };
    return G;
  }

  boolean hornImplied(int j, boolean[] G, int[][] body, int[] head) {
    if (G[j]) { return false; };
    int c = 0;
    while (c < body.length) {
      if (head[c] == j) {
        boolean allTrue = true;
        int k = 0;
        while (k < body[c].length) {
          if (!G[body[c][k]]) { allTrue = false; };
          k = k + 1;
        };
        if (allTrue) { return true; }
      };
      c = c + 1;
    };
    return false;
  }
}

LLP predicates for this chapter

Each LLP program in this chapter defines a state vector $G$ and a forbidden predicate; the algorithm runs until no $j$ is forbidden. The table below lists, for each algorithm, what $G[j]$ represents and the negation of the forbidden clause from the matching .llp source.