Events
e120December 14, 2011  Presentation: Correctness proof of DavisPutnam and DavisPutnamLovgemannLoveland algorithm 
Room: Zi 5126  Matej Mihelčić 
13:3014:30  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), DavisPutnam (DP) and DavisPutnamLogemannLoveland (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.
