Presentation: Correctness proof of Davis-Putnam and Davis-Putnam-Lovgemann-Loveland algorithm
When: Dec. 14, 2011, 13:30-14:30
Where: Zi 5126
Who: Matej Mihelčić
Satisfiability problem is one of the most researched problems in computer science because of it's numerous practical applications and significant theoretical impact, especially in complexity theory. In this presentation we will shortly introduce some basic concepts of propositional logic and describe resolution rule.
We will present two complete algorithms for solving Satisfiability problem (SAT), Davis-Putnam (DP) and Davis-Putnam-Logemann-Loveland (DPLL) algorithm. Short description of correctness proof for each of these algorithms will be presented.
We will define interaction graph and show on example how to represent a logical formula via the interaction graph.