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.

	Home > News and Events > Events
<< EEMCS (EWI) Home News and Events » Group Colloquium » Events » In the Media People Research Education Vacancies Intranet Contact	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.