In this weeks theory seminar, we’ll have Oliver Kullmann give a presentation entitled ‘Classification of minimally unstaisfiable 2-CNFs, and applications’.

Abstract

How do unsatisfiable 2-CNFs look like “at the core”, that is, without superfluous clauses? With my student Hoda Abbasizanjani we achieved a complete classification, where finally I was able to complete all proofs, and so I can present to you this nice piece of foundational work. (The proofs use various aspects of automorphisms of (combinatorial) graphs, and that field is full of “hand waving”, which is quite hard to eliminate.) With a collaborator from industry, we started exploiting these results, in the direction of “explaining causes of unsatisfiability”, and I can sketch that as well.