Logik in der Informatik Prof. Dr. Martin Grohe

Institut für Informatik

SAT solving on formulas of bounded tree-width

Tree-width is a measure that indicates how tree-like a graph or a logical formula is. Like many other NP-problems, SAT can be solved in polynomial time if it is restricted to instances that have bounded tree-width. In this talk I will prove this result, by presenting different algorithmic approaches that make use of a Tree Decomposition. This work was done during my diploma thesis under the supervision of Prof. Martin Grohe.