Horn Formulas

Boolean variables take true or false values which can be negated. A literation is a variable, or its negation.

In horn formulas, there are two types of clauses:

1. Implications $A⟹B$
   1. Here, $A$ is a and of any number of positive literals
   2. $B$ is a single positive literal
2. Pure negative clause: an or of any number of negative literals

Given a horn formula, can we assign a true / false value to each variable such that all clauses are true? This leads to SAT.

We can use a greedy algorithm to try to solve this:

Greedy Algorithm:
Input: a Horn formula
Output: a satisfying assignment, if one exists
set all variables to false
while there is an implication clause that is not satisfied:
    set the right-hand variable of the implication to true
if all pure negative clauses are satisfied:
    return satisfying assignment
else:
    return "formula unsatisfiable"

Note

If a variable is set to true by the algorithm, then it must be true in any satisfying assignment. This can be proved by induction.