On Minimally Unsatisfiable Conjunctive Normal Forms

Oliver Kullmann

Supported by the Natural Sciences and Engineering Research Council of Canada and by the Communications and Information Technology Ontario.

We give an overview on recent progress towards an understanding of the structure of minimally unsatisfiable clause-sets, focussing on the notion of deficiency δ(F) = c(F) − n(F) ([4]), where c(F) is the number of clauses and n(F) is the number of variables, and considering also generalisations like lean clause-sets ([5]), which are clause-sets without non-trivial autarkies.

Starting with [1], where δ(F) ≥ 1 for minimally unsatisfiable F has been shown, and the class of “saturated” minimally unsatisfiable F with δ(F) = 1 has been characterised, one central problem has been the classification of minimally unsatisfiable clause-sets with small deficiency. In [3] the class of all minimally unsatisfiable F with δ(F) = 1 is characterised, and in [2] an upper bound for tree-like resolution depending on the deficiency is given. In [6] for all k the decision problem for minimally unsatisfiable F with δ(F) ≤ k has been shown to be in polynomial time (see also [7] for further developments).

[1] Ron Aharoni and Nathan Linial. Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas. Journal of Combinatorial Theory, A 43:196–204, 1986.

[2] Hans Kleine Büning. An upper bound for minimal resolution refutations. In Georg Gottlob, Etienne Grandjean, and Katrin Seyr, editors, Computer Science Logic 12th International Workshop, CSL’98, volume 1584 of Lecture Notes in Computer Science, pages 171–178. Springer, 1999.

[3] Gennady Davydov, Inna Davydova, and Hans Kleine Büning. An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF. Annals of Mathematics and Artificial Intelligence, 23:229–245, 1998.

[4] John Franco and Allen Van Gelder. A perspective on certain polynomial time solvable classes of satisfiability. To appear in Discrete Applied Mathematics, 2000.

[5] Oliver Kullmann. Investigations on autark assignments. Submitted to Discrete Applied Mathematics, 1998.

[6] Oliver Kullmann. An application of matroid theory to the SAT problem. Technical Report TR00-018, Electronic Colloquium on Computational Complexity (ECCC), March 2000.

[7] Oliver Kullmann. On structural properties of minimally unsatisfiable clause-sets. In preparation, January 2000.

Address: Department of Computer Science, University of Toronto, Toronto, Ontario M5S 3G4, Canada

E-mail: kullmann@cs.toronto.edu