Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

The following is an algorithm to find truth assignments for Horn Formulas:

Input: A Horn Formula

Output: A satisfying assignment, if one exists

  • Set all variables to false
  • While there is an implication that is not satisfied: Set the right hand variable of the implication to true
  • If all pure negative clauses are satisfied: Return the assignment.
  • Else: Return "Formula is not satisfiable"

The book Algorithms defines a Horn Formula as a formula that consists of implications (left hand side is an AND of any number of positive literals and whose right hand is a single positive literals) and pure negative clauses, consisting of an OR of any number of negative literals.

Will the above algorithm work to identify truth assignments for expressions that are not Horn Formulas? For example, if a logic expression consists of combinations of positive literals and negative literals (and therefore violates the Horn Formula requirement for all expressions to be either implications or pure negative clauses), would this algorithm still work?

E.g: $(v_1∧ \bar{v_2} ∧v_3 )⇒v_4 ∧ v_5 $

The above expression is clearly not a Horn Formula: would the algorithm still be valid with these kind of expressions? If the algorithm does work on any logical expression set, then what makes Horn Formulas special? (since the generalization of the above algorithm would mean a linear time solution for all truth assignments as opposed to a linear time solution for only Horn Formulas)

share|improve this question

1 Answer 1

I doubt you can generalise your algorithm for arbitrary clauses, since arbitrary satisfiability is NP-complete whereas your algorithm is linear.

To understand why the algorithm works for Horn clauses let us identify a variable assignment $M$ with the set of variables that are assigned the value $true$. Consider a set $A$ of Horn clauses and let $A = D \cup N$, where $D$ is the set of definite clauses (clauses with exactly one negative variable) and $N$ is the set of all negative clauses.

Now any set of definite clauses has a least variable assignment (in the set inclusion order) that satisfies it. In the first part of your algorithm you construct the least variable assignment $M$ for $D$.

If $M'$ is a variable assignment that satisfies $A$, then it satisfies $D$ and so $M \subseteq M'$. But since the clauses in $N$ are all negative $M$ also satisfies $N$. Thus if $A$ is satisfiable then it is satisfied by $M$. So in the second part of the algorithm you just check whether $M$ satisfies $N$.

share|improve this answer
    
I understand why the algorithm works for Horn Clauses. Could you explain why it doesn't work for arbitrary clauses? (e.g. Possibly provide an example for arbitrary clauses) –  user26649 Aug 13 '12 at 17:31
    
The clause $v_1 \lor v_2$ for example does not have a least model. If you transform it to the implication $\lnot v_1 \to v_2$, then your algorithm will assign the value $true$ to $v_2$. Thus according to the algorithm the set $\{\lnot v_1 \to v_2, \lnot v_2\}$ is not satisfiable. But that is not correct. –  Levon Haykazyan Aug 13 '12 at 18:52

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.