Horn Clauses and Horn Formulas
Horn Clauses and Horn Formulas
We now define a class of clauses (formulas) for which there is an efficient algorithm for deciding satisfiability for sets of clauses (formulas) from the class.
Definition
A Horn clause is a clause in which at most one of the literals is a non-negated propositional variable.
Example
{P, ¬Q, ¬R}, {¬P, ¬Q, ¬R}, and {S} are Horn clauses. {P, Q, ¬S} is not a Horn clause.
Definition
A Horn formula is a formula of the form. P, ¬(P1 ∧ . . . ∧ Pn) for n ≥ 1, or ((P1 ∧ . . . ∧ Pm) → Q) for m ≥ 1.
Question
Which of the following are Horn clauses?
{¬S}
{¬P, ¬Q, R, ¬S}
{Q, R, S}
{R}
{P, ¬Q, R, ¬S}
{¬P, ¬Q, ¬R}
Horn Clauses and Horn Formulas
Notice that
¬(P1 ∧ . . . ∧ Pn) ⊨ (¬P1 ∨ . . . ∨ ¬Pn)
and that
((P1 ∧ . . . ∧ Pm) → Q) ⊨ (¬(P1 ∧ . . . ∧ Pm) ∨ Q) ⊨ (¬P1 ∨ . . . ∨ ¬Pm ∨ Q)
So we associate a Horn clause of the form. {P} with the Horn formula P, associate a Horn clause of the form. {¬P1, . . . , ¬Pn} with the Horn formula ¬(P1 ∧ . . . ∧ Pn), and associate a Horn clause of the form. {¬P1, . . . , ¬Pm, Q} with the Horn formula ((P1 ∧ . . . ∧ Pm) → Q).
Since we can associate Horn clauses with Horn formulas, we will describe our satisfiability algorithm only for sets of Horn formulas.
Question
Write down the associated Horn formula for each of the following Horn clauses.
{¬S}
{¬P, ¬Q, R, ¬S}
{R}
{¬P, ¬Q, ¬R}
Satisfiability for Sets of Horn Formulas
Given a set Γ of Horn formulas, the following algorithm either defines a truth assignment e that satisfies Γ or concludes that Γ is unsatisfiable.
Each step of the algorithm reads each formula at most once, and it either defines e on one more variable or halts. Thus, the algorithm is efficient.
Satisfiability for Sets of Horn Formulas