Editing Horn-satisfiability (section)

==Algorithm==

The problem of Horn satisfiability is solvable in [[linear time]].<ref>{{citation
 | last1 = Dowling | first1 = William F.
 | last2 = Gallier | first2 = Jean H. | author2-link = Jean Gallier
 | doi = 10.1016/0743-1066(84)90014-1
 | issue = 3
 | journal = Journal of Logic Programming
 | mr = 770156
 | pages = 267–284
 | title = Linear-time algorithms for testing the satisfiability of propositional Horn formulae
 | volume = 1
 | year = 1984| doi-access = free
 }}</ref> 
A polynomial-time algorithm for Horn satisfiability is [[Recursion (computer science)|recursive]]:
* A first termination condition is a formula in which all the clauses currently existing contain negative literals. In this case, all the variables currently in the clauses can be set to false.
* A second termination condition is an empty clause. In this case, the formula has no solutions.
* In the other cases, the formula contains a positive unit clause <math>l</math>, so we do a [[unit propagation]]: the literal <math>l</math> is set to true, all the clauses containing <math>l</math> are removed, and all clauses containing <math>\neg l</math> have this literal removed. The result is a new Horn formula, so we reiterate.

This algorithm also allows determining a truth assignment of satisfiable Horn formulae: all variables contained in a unit clause are set to the value satisfying that unit clause; all other literals are set to false. The resulting assignment is the minimal model of the Horn formula, that is, the assignment having a minimal set of variables assigned to true, where comparison is made using set containment.

Using a linear algorithm for unit propagation, the algorithm is linear in the size of the formula.

===Examples===
====Trivial case====
In the Horn formula
:{{math|(¬''a''&nbsp;∨&nbsp;¬''b''&nbsp;∨&nbsp;''c'')&nbsp;∧}}
:{{math|(¬''b''&nbsp;∨&nbsp;¬''c''&nbsp;∨&nbsp;''d'')&nbsp;∧}}
:{{math|(¬''f''&nbsp;∨&nbsp;¬''a''&nbsp;∨&nbsp;''b'')&nbsp;∧}}
:{{math|(¬''e''&nbsp;∨&nbsp;¬''c''&nbsp;∨&nbsp;''a'')&nbsp;∧}}
:{{math|(¬''e''&nbsp;∨&nbsp;''f'')&nbsp;∧}}
:{{math|(¬''d''&nbsp;∨&nbsp;''e'')&nbsp;∧}}
:{{math|(¬''b''&nbsp;∨&nbsp;¬''c'')}},

each clause has a negated literal. Therefore, setting each variable to false satisfies all clauses, hence it is a solution.

====Solvable case====
In the Horn formula
:{{math|(¬''a''&nbsp;∨&nbsp;¬''b''&nbsp;∨&nbsp;''c'')&nbsp;∧}}
:{{math|(¬''b''&nbsp;∨&nbsp;¬''c''&nbsp;∨&nbsp;''f'')&nbsp;∧}}
:{{math|(¬''f''&nbsp;∨&nbsp;''b'')&nbsp;∧}}
:{{math|(¬''e''&nbsp;∨&nbsp;¬''c''&nbsp;∨&nbsp;''a'')&nbsp;∧}}
:{{math|(''f'')&nbsp;∧}}
:{{math|(¬''d''&nbsp;∨&nbsp;''e'')&nbsp;∧}}
:{{math|(¬''b''&nbsp;∨&nbsp;¬''c'')}},

one clause forces ''f'' to be true. Setting ''f'' to true and simplifying gives
:{{math|(¬''a''&nbsp;∨&nbsp;¬''b''&nbsp;∨&nbsp;''c'')&nbsp;∧}}
:{{math|(''b'')&nbsp;∧}}
:{{math|(¬''e''&nbsp;∨&nbsp;¬''c''&nbsp;∨&nbsp;''a'')&nbsp;∧}}
:{{math|(¬''d''&nbsp;∨&nbsp;''e'')&nbsp;∧}}
:{{math|(¬''b''&nbsp;∨&nbsp;¬''c'')}}.

Now ''b'' must be true.  Simplification gives
:{{math|(¬''a''&nbsp;∨&nbsp;''c'')&nbsp;∧}}
:{{math|(¬''e''&nbsp;∨&nbsp;¬''c''&nbsp;∨&nbsp;''a'')&nbsp;∧}}
:{{math|(¬''d''&nbsp;∨&nbsp;''e'')&nbsp;∧}}
:{{math|(¬''c'')}}.

Now it is a trivial case, so the remaining variables can all be set to false. Thus, a satisfying assignment is
:{{math|1=''a''&nbsp;=&nbsp;false}},
:{{math|1=''b''&nbsp;=&nbsp;true}},
:{{math|1=''c''&nbsp;=&nbsp;false}},
:{{math|1=''d''&nbsp;=&nbsp;false}},
:{{math|1=''e''&nbsp;=&nbsp;false}},
:{{math|1=''f''&nbsp;=&nbsp;true}}.

====Unsolvable case====
In the Horn formula
:{{math|(¬''a''&nbsp;∨&nbsp;¬''b''&nbsp;∨&nbsp;''c'')&nbsp;∧}}
:{{math|(¬''b''&nbsp;∨&nbsp;¬''c''&nbsp;∨&nbsp;''f'')&nbsp;∧}}
:{{math|(¬''f''&nbsp;∨&nbsp;''b'')&nbsp;∧}}
:{{math|(¬''e''&nbsp;∨&nbsp;¬''c''&nbsp;∨&nbsp;''a'')&nbsp;∧}}
:{{math|(''f'')&nbsp;∧}}
:{{math|(¬''d''&nbsp;∨&nbsp;''e'')&nbsp;∧}}
:{{math|(¬''b'')}},

one clause forces ''f'' to be true.  Subsequent simplification gives
:{{math|(¬''a''&nbsp;∨&nbsp;¬''b''&nbsp;∨&nbsp;''c'')&nbsp;∧}}
:{{math|(''b'')&nbsp;∧}}
:{{math|(¬''e''&nbsp;∨&nbsp;¬''c''&nbsp;∨&nbsp;''a'')&nbsp;∧}}
:{{math|(¬''d''&nbsp;∨&nbsp;''e'')&nbsp;∧}}
:{{math|(¬''b'')}}.

Now ''b'' has to be true. Simplification gives
:{{math|(¬''a''&nbsp;∨&nbsp;''c'')&nbsp;∧}}
:{{math|(¬''e''&nbsp;∨&nbsp;¬''c''&nbsp;∨&nbsp;''a'')&nbsp;∧}}
:{{math|(¬''d''&nbsp;∨&nbsp;''e'')&nbsp;∧}}
:{{math|()}}.
We obtained an empty clause, hence the formula is unsatisfiable.