Horn clauses and satisfiability

Horn formulas are conjunctions of Horn clauses. Horn clauses are an implication whose assumption (left side of the arrow) A is a conjunction of the proposition of type P and whose conclusion (right side of the arrow) is of type P (P::= ┴ | ┬| atom) also. Here is shown a Horn formula, having conjunctions of Horn clauses.

H = (p → q)∧ (t∧ r → ┬) ∧ (p ∧ r ∧ s → ┴)

A Horn formula is a formula φ of propositional logic if it can be generated as an instance of H in this grammar:

P::= ┴|┬| p

A::= P | P ∧ A

C::= A → P

H::= C | C ∧ H

We call each instance of C a Horn clause.

In other words:

– 1 or more clauses separated by AND.

 – Each clause must have:

• NO negations.
• One implication.
• The left-hand side of implication:
  • can be one or more of propositions of type P (P::= ┴| T | atom) separated by an AND.
• The right-hand side of implication:
  • Must be one of type P (P::= ┴ | T | atom).

A formula is a Horn formula if it is in CNF and every disjunction contains at most one positive literal. Horn clauses are clauses, which contain at most one positive literal.

• H=(p V ¬q) ∧ (¬c V ¬p V q) ∧ (¬t V ¬r) ∧ d
• H =(q → p) ∧ (c ∧ p → q) ∧ (t ∧ r → ┴) ∧ (T →d)

Examples of Horn formulas are:

• (p ∧ q ∧ s → p) ∧ (q ∧ r → p) ∧ (p ∧ s → s)
• (p ∧ q ∧ s → ┴) ∧ (q ∧ r → p) ∧ (┬→ s)
• (p₂ ∧ p₃ ∧ p₅ → p₁₃) ∧ (┬ → p₅) ∧ (p₅ ∧ p₁₁ → ┴)

Examples of formulas which are not Horn formulas:

• (p ∧ q ∧ s → ¬p) ∧ (q ∧ r → p) ∧ (p ∧ s → s)
• (p ∧ q ∧ s → ┴) ∧ (¬q ∧ r → p) ∧ (┬ → s)
• (p₂ ∧ p₃ ∧ p₅ → p₁₃ ∧ p₂₇) ∧ (┬ → p₅) ∧ (p₅ ∧ p₁₁ → ┴)
• (p₂ ∧ p₃ ∧ p₅ → p₁₃ ∧ p₂₇) ∧ (┬ → p₅) ∧ (p₅ ∧ p₁₁ ∨ ┴)

The first formula is not a Horn formula since ¬p, the conclusion of the implication of the first conjunct is not of type P(P::= ┴ | T | atom). The second formula does not qualify since the premise of the implication of the second conjunct, ¬q ∧ r, is not a conjunction of type P(P::= ┴| T | atom). The third formula is not a Horn formula since the conclusion of the implication of the first conjunct, p₁₃ ∧ p₂₇, is not of type P(P::= ┴| T | atom). The fourth formula is not a Horn formula since it is not a conjunction of implications.

The test for the satisfiability of a class of formulas is very hard in general. Fortunately, there are some important subclasses of formulas which have much more efficient ways of deciding their satisfiability. One such example of the classes of formulas is the class of Horn formulas; the name ‘Horn’ is derived from the logician’s last name; named A. Horn. We shortly define them and give an algorithm for checking their satisfiability.

Horn formula allows computing satisfiability, efficiently. If a set of formulas is not satisfiable, there is a contradiction/inconsistency in the rules.

The Algorithm to test for Satisfiability

Function HORN (f)

//precondition: f is a Horn formula

//postcondition: HORN (f) decides the satisfiability for f

{

      mark all occurrences of T in f

      while there is a conjunct p₁ ∧ p₂ ∧ … p_n → P of f, such that all p_j are marked but P is not

            Mark P

      end while

      if ┴ is marked

            return ‘unsatisfiable’

      else

            return ‘satisfiable’

     end if

}

Horn clauses examples

Exercise 1

(T→ q) ∧ (T → s) ∧ (w →┴) ∧ (p∧q∧s→v) ∧ (v→s) ∧ (T→r) ∧(r→p)

Mark: q, s, r through (T→q),(T→s),(T→r)

(T→ q) ∧ (T → s) ∧ (w →┴) ∧ (p∧q∧s→v) ∧ (v→s) ∧ (T→r) ∧(r→p)

Mark: p through (r→p)

(T→ q) ∧ (T → s) ∧ (w →┴) ∧ (p∧q∧s→v) ∧ (v→s) ∧ (T→r) ∧(r→p)

Mark: v through (p∧q∧s→v)

(T→ q) ∧ (T → s) ∧ (w →┴) ∧ (p∧q∧s→v) ∧ (v→s) ∧ (T→r) ∧(r→p)

Return?

– Satisfiable

Exercise 2

(p∧q∧s→p) ∧ (q∧r→p) ∧ (p∧s→s)

No occurrences of T in f

Nothing is marked

Returning: Satisfiable

Exercise 3

(p∧q∧s→p) ∧ (q∧r→p) ∧ (p∧s→s)

 Remember that a formula f is satisfiable if there is an interpretation that makes the formula f true.

Let p, q, r, s be false, then

• (p∧q∧s→p) is True (false implying anything is True),
• (q∧r→p) is True
• (p∧s→s) is True
• The formula is True

Exercise 4

(p∧q∧s→┴) ∧ (q∧r→┴) ∧ (s→┴)

No occurrences of T in f

Nothing is marked

Returning: Satisfiable

When p, q, r, s are false, the formula is True

 

The conjunctive normal form-Disjunctive normal form