LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision Both sides next revision
sav08:polynomial_algorithm_for_horn_clauses [2008/03/12 01:41]
vkuncak
sav08:polynomial_algorithm_for_horn_clauses [2008/03/12 10:43]
vkuncak
Line 8: Line 8:
  
 To check satisfiability of a set of Horn clauses: To check satisfiability of a set of Horn clauses:
-  * while the set contains a clause of the form $\{p\}$ where $p$ is a propositional variable:+  * while the set contains a clause of the form $\{p\}$ where $p$ is a propositional variable, do //boolean constraint propagation//​:
      * erase all clauses that contain literal $p$       * erase all clauses that contain literal $p$ 
-     * remove $\lnot p$ from all literals +     * remove $\lnot p$ from all clauses 
-     * if there is an empty clause, set is not satisfiable +     * if there is an empty clause, ​the set is unsatisfiable 
-  * if no contradiction ​found, the set is satisfiable+  * if no empty clause ​found after repeating the above, the set is satisfiable
  
-On $\{p\}$ we conclude that $p$ must be true and derive valid consequences of this fact.  If we obtain contradiction,​ the set of clearly ​unsatisfiable.+Boolean constraint propagation is a sound inference rule.  If we obtain contradiction,​ the set is therefore ​unsatisfiable.
  
-Moreover, if loop terminates and there are no empty clauses, then every clause contains a negative literal. ​ The assignment that sets all remaining variables to //false// is a satisfying assignment.+If loop terminates and there are no empty clauses, then every clause contains a negative literal. ​ The assignment that sets all remaining variables to //false// is a satisfying assignment.
  
 This algorithm does polynomial amount of work for each propositional variable, so it is polynomial. This algorithm does polynomial amount of work for each propositional variable, so it is polynomial.