Research Topic (nur in Englisch)

---

General Informations

Funded by: Deutsche Forschungsgemeinschaft (DFG) (National Research Foundation).

Project Manager:

• Prof. Dr. Hans Kleine Büning
• Xishun Zhao, Zhongshan University, Guangzhou, P.R.China
• Daoyun Xu

---

Abstract

Within this project we deal with minimal unsatisfiable formulas of propositional logic given in conjunctive normal form, MU-formulas for short. Every unsatisfiable propositional formula in CNF contains in the core at least one MU-formula. Therefore, these formulas play a prominet role in testing the efficiency of algorithms deciding satisfiability or deriveability. Commonly, MU-formulas are classified by the difference between number of clauses n+k and number of variables n. This project aims in finding (structural) characterizations for classes MU(k) of MU-formulas with fixed clause-variable-difference k. Based on these characterizations, we will try to formulate algorithms that decide the classes MU(k) efficiently.

---

Selected Publications

An introduction into this subject is given in an internal report (downloadable from this page). Most of the results achieved within this project have been published or will appear soon. Preversions can be looked up here.

• H. Kleine Büning, X. Zhao: Minimal Unsatisfiability: Results and Open Questions. Technical Report tr-ri-02-230, University of Paderborn, 2002. [pdf]

---

Enumerating Minimal Unsatisfiable Formulas

In order to characterize the structure of MU-formulas it is essential to have a nontrivial number of examples. Such examples can be found in a generate-and-test manner using some random generator for formulas (e.g. in the fixed clause length model) and an efficient implementation of the DPLL-procedure. Once an unsatisfiable instance is found, it can be reduced to a MU-formula by deleting clauses until satisfiability is achieved. Unfortunately, we cannot predict the clause-variable-difference k of the resulting MU-formula. As a further weakness of this approach we cannot expect that the resulting formulas are uniformly distributed samples of the class MU.

Alternatively, we can try to generate MU-formulas from scratch in an inductive manner using the number of variables for the induction step. In this way the classes MU(k,n) can be determined, containing all MU(k)-formulas with n variables. For enumerating the candidate formulas the splitting theorem is used: Any MU(k,n)-formula can be decomposed into two MU-formulas belonging to classes MU(k',n') and MU(k",n") with k',k" <= k and n',n" <= n (see Technical Report, page 6 for details). So, new MU-formulas can be generated by overlapping and introducing a new variable from MU-formulas already known. Unfortunately, this approach also is impractical, since the number of MU-formulas increases quickly.

The following tabular gives the number of different MU(k,n)-formulas (up to isomorphism, i.e. permutation of variable names and swapping negation signs of all occurrences of variables).

MU(k,n)		k
		1	2	3	4	5	6	7	8	9	10	11	12
n	0	1
	1	1
	2	2	1
	3	10	12	13	3	1
	4	86	365	1609	5602	124056	194464	145357	90752	20869	3673	169	1
	5	1594	126130	???	???	???	???	???	???	???	???	???	???
	6	51825	???	???	???	???	???	???	???	???	???	???	???

You can download the formula samples by clicking onto the corresponding entry of the above tabular. The formulas are listed in the following format: First, a unique number a formula is given, together with the numbers of its parents (the formulas from which it was created by reverse splitting). Then, the clauses are listed, separated by bracketing. The atoms are named by numbers in the range 1..n, each number in that range occurs. The minus sign is used as negation sign. See the following example:

131:6:2
(2)
(-3)
(1,4)
(1,-4)
(-1,-4)
(-1,-2,3,4)

Formula files are compressed (using gzip), but nevertheless they are quite large.