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)