Understanding unsatisfiability?!

Oliver Kullmann, Swansea University. Part of the algebra, logic and algorithms seminar series.

I will present recent work with my student Hoda Abbasizanjani on classifying minimal unsatisfiable formulas.  I will discuss the two most fundamental layers of unsatisfiable CNFs (tautological DNFs), given by the simplest form of the expansion rule and by "cyclic reasoning".

Only very basic knowledge about propositional logic is required.