Notes - Logic and Proof MT24, Horn formulas


Flashcards

What is a Horn clause?


A disjunctive clause with at most one positive literal.

What is a disjunctive clause with at most one positive literal called?


A Horn clause.

What is a Horn formula?


A conjunction of Horn clauses, which are disjunctive clauses containing at most one positive literal.

What is the head of a Horn clause?


The positive literal.

What is the body of a Horn clause?


The disjunction of the negative literals.

How could you more intuitively rewrite the Horn formula

\[p_1 \land (\lnot p_2 \lor \lnot p_3) \land (\lnot p_1 \lor \lnot p_2 \lor p_4)\]

?


As conjuncts of implications where the body implies the head:

\[(\mathbf{true} \to p_1) \land (p_2 \land p_3 \to \mathbf{false}) \land (p_1 \land p_2 \to p_4)\]

Suppose that $F$ is a Horn formula in “implication form”. Describe an @algorithm which can determine whether a Horn formula $F$ is satisfiable in polynomial time.


  • $v := \mathbf 0$, initialise a zero valuation
  • While $v$ does not satisfy $F$:
    • Pick an unsatisfied clause $p _ 1 \land \cdots \land p _ k \to G$
    • If $G$ is a variable:
      • Set $v[G] = 1$ and continue
    • Else:
      • Return “unsatisfiable”
  • Return $v$

If $F$ is a Horn formula in “implication form” over $n$ propositional variables, then an algorithm to decide whether it is satisfiable is given by:

  • $v := \mathbf 0$, initialise a zero valuation
  • While $v$ does not satisfy $F$:
    • Pick an unsatisfied clause $p _ 1 \land \cdots \land p _ k \to G$
    • If $G$ is a variable:
      • Set $v[G] = 1$ and continue
    • Else:
      • Return “unsatisfiable”
  • Return $v$

@Prove that this is a valid polynomial time algorithm, and that this algorithm actually returns a minimum model of a Horn formula $v$.


If there are $n$ clauses, there can be at most $n$ iterations and so the algorithm terminates in time polynomial in the size of the input formula.

If the formula is satisfiable then the condition of the while loop means that the algorithm will terminate with a satisfying assignment.

So it remains to show that if the algorithm returns “unsatisfiable”, then the formula $F$ really is unsatisfiable.

Suppose that there is an assignment $v’$ that satisfies $F$. Then $v \le v’$ is a loop invariant.

  • Initialisation: $v = 0$ establishes the invariant.
  • Maintenance:
    • Suppose that the invariant holds at the beginning of the loop, and consider an arbitrary unsatisfied clause $p _ 1 \land \cdots \land p _ k \implies G$.
    • This implies that $p _ 1 \land \cdots \land p _ k$ is satisfied by $v’$ but $G$ is not satisfied by $v$.
    • Since $v \le v’$, $v’$ also satisfies $p _ 1, \ldots, p _ k$.
    • Then $v’$ satisfies $G$, so $G \ne \mathbf{false}$, and so the algorithm won’t return “unsatisfiable”
    • Since $v’[G] = 1$, setting $v[G] = 1$ preserves the invariant.
  • Conclusion: If the algorithm terminates, then $F$ is satisfied and $v \le v’$. Since $v \le v’$ for any satisfying assignment $v’$, it follows $v$ is a minimum model of $F$.

(here the loop invariant together with the negation of the while loop condition isn’t used to establish correctness. Instead the invariant is chosen since it allows you to conclude that if a satisfying assignment exists, then the algorithm won’t ever return “unsatisfiable”, since $G$ won’t be $\mathbf{false}$).




Related posts