A method of generating minimally unsatisfiable conjunctive normal forms is introduced. A conjunctive normal form (CNF) is minimally unsatisfiable if it is unsatisfiable and such that removing any one of its clauses results in a satisfiable CNF.

Introduction

Ivor Spence [1] introduced a method for producing small unsatisfiable formulas of propositional logic that were difficult to solve by most SAT solvers at the time, which we believe was because they were usually minimally (i.e. just barely) unsatisfiable. Kullmann and Zhao [2] claim that minimally unsatisfiable formulas are “the hardest examples for proof systems.” We will generalize Spence’s construction and show that it can be used to generate minimally unsatisfiable propositional formulas in conjunctive normal form, that is, formulas that are unsatisfiable but such that the removal of even a single clause produces a satisfiable formula. In addition to increasing our understanding of the satisfiability problem, these formulas have important connections to other combinatorial problems [3].

Definitions

We assume the reader has at least a minimal acquaintance with propositional logic and truth tables. An interpretation of a propositional formula is an assignment of truth values to its propositional variables. A propositional formula is satisfiable if there is an interpretation that makes it true when evaluated using the usual truth table rules. A literal is a propositional variable or a negated propositional variable. A clause is a disjunction of literals; if it contains exactly literals, we call it a -clause. A conjunctive normal form (or CNF) is a conjunction of clauses. A -CNF is a conjunction of -clauses.

For example, is a 3-CNF. It is often convenient to think of CNFs as a list of lists of literals; in this format, the 3-CNF example would be written as . This way of writing CNFs is quite common in computer science and is the approach that we took in [4], where we showed how the famous Davis–Putnam algorithm for satisfiability testing could be easily programmed in Mathematica. , Mathematica’s built-in function for satisfiability testing, requires replacing “¬” by “!”, “∨” by “||” and “∧” by “&&”; so in Mathematica the 3-CNF example is written as . In this article, we adopt the “list of lists” approach for programming purposes and then convert to Mathematica’s format when testing for satisfiability with .

Constructing Unsatisfiable CNFs

In this section, we show how to generalize a construction of Ivor Spence [1] that produces unsatisfiable 3-CNFs that are relatively short but take a relatively long time to verify that they are indeed unsatisfiable using standard computer programs, even though it is relatively easy, as we shall show, to demonstrate that they are unsatisfiable. (Perhaps humans are not replaceable by computers, after all!)

Given positive integers and , suppose the propositional variables , , …, are partitioned in order into sets of size and one set of size . For each cell of the partition, form all -clauses from the ’s in that cell and let be the conjunction of all these -clauses. If is to be true under an interpretation , no more than of the -variables from each partition cell can be false, since if were false, the -clause containing exactly these -variables would be false, as would their conjunction . Thus no more than of the -variables can be false under .

Next let, , …, be a random permutation of the ’s and partition these ’s just as the ’s were partitioned. However, this time, for each cell of the partition, form all -clauses from the negated -variables in that cell and let be the conjunction of all these -clauses. Reasoning as before, no more than -variables can be true under .

Let . If is to be true under some interpretation , both and must be true under ; thus no more than -variables can be false and no more than -variables can be true under . Since the -variables are permuted -variables, it follows that no more than -variables can be true under . However, , the number of -variables in ! Thus is an unsatisfiable CNF, because there is no interpretation of all its -variables that makes true.

Minimally Unsatisfiable CNFs

Suppose next that we drop one of the clauses in , say for example, ; let and let . Let be an interpretation that assigns false to , , …, and true to the remaining variables in the first -cell. As long as no more than -variables in each of the remaining cells of the partition of the ’s are assigned the value false, would be true under . Whether or not and hence are true under depends on whether also has the property that at most -variables in each cell of the partition of the randomly permuted variables (the ’s) are assigned the value true under . While this is unlikely for any given interpretation , there are so many interpretations satisfying that it is most likely that some such interpretation has this property and the reduced CNF will then be true under .

We will investigate this intuitive argument. For to be true, the -variables , , …, can now be false in the first cell, as long as each of the remaining cells in the -partition has at most false variables; thus -variables can be false and, as above, -variables can be true. However, , and the argument showing to be unsatisfiable cannot be applied to .

Programming

First we allow for different choices for the parameters and . Initially we set and . The next several steps serve to introduce the variables and partition them into cells.

Define the partition of the -variables.

Here is the -partition for our example.

Next we generate, negate and partition the -variables.

We join and and form all -sets from the result.

puts these steps together. The argument is a permutation of .

For the experiments that follow, leaving out the third argument uses a random permutation.

Because of , the negated pieces can change from one run to the next.

The function transforms a list of clauses into an expression that allows for satisfiability testing, as described in the section Definitions.

Equivalently, here is a longer form.

To test that a CNF is minimally unsatisfiable, we must show both that it is unsatisfiable and that the removal of any one clause always results in a satisfiable CNF. tests the satisfiability of a CNF in list form by converting it to a logical expression with and applying the built-in function ; then it tests if all the formulas with one clause deleted are indeed satisfiable.

This tests whether C3 is minimally unsatisfiable.

Most of the unsatisfiable formulas generated in this way are, as we shall see, minimally unsatisfiable, but not always. However, we conjecture that the bigger we take and , the more likely we are to get a minimally unsatisfiable formula. We have done some experiments on this conjecture and discuss them in the next section.

If we remove two different clauses instead of one from our unsatisfiable formulas, the result is almost always a satisfiable formula. We define the function and experiment with it in the next section.

Experiments

We run some experiments to investigate the frequency of minimally unsatisfiable CNFs obtained with our Spence generalizations.

The table below summarizes some larger computer experiments we have conducted to test our conjecture that most of the formulas constructed by the above methods are minimally unsatisfiable. The third column, “”, stands for the number of clauses in the CNF defined by SpenceCNF@SpenceList[k,g]. The fourth column gives the percentage of these clauses that were minimally unsatisfiable.

Each line in the table represents results on 500 formulas. For example, the first line constructs 500 3-CNFs, based on variables and clauses in each. It turned out that 62% were minimally unsatisfiable.

Next we look at what happens if we remove two different clauses from our Spence formulas. With , , there are 92 clauses in the Spence CNF; hence distinct ways to remove two different clauses. We count the number of times the resulting CNF is true in 100 trials.

In this trial, we are very close to all Spence CNFs becoming satisfiable after removing two different clauses. We believe this is true in general.

Derangements

In this section we modify our construction to generate only derangements of the -variables. A derangement is a permutation that leaves no number in its original position. There are three resource functions that deal with derangements.

It is known that derangements constitute slightly more than a third of the permutations (see [5]), as the following calculation illustrates.

We define the function that does “derangement” experiments.

On the basis of these experiments we conjecture that the derangements are about as likely to produce minimally unsatisfiable formulas as permutations in general.

Conclusion

We have adapted a method of I. Spence [1] to easily obtain large numbers of unsatisfiable CNFs that are usually but not always minimally unsatisfiable. We also ran some experiments to indicate what percentages would be minimally unsatisfiable. In addition, our experiments suggest that if two different clauses are removed rather than one, the resulting formula will almost always be satisfiable. Finally we restricted the random permutations in our construction by requiring them to be derangements and saw that this gave similar percentages of minimally unsatisfiable formulas.

Acknowledgements

I am grateful to the referee for his advice and to the editor, George Beck, for greatly improving my Mathematica coding throughout the paper.

References

[1]	I. Spence, “sgen1: A Generator of Small but Difficult Satisfiability Benchmarks,” ACM Journal of Experimental Algorithmics, 15, 2010 pp. 1.1–1.15. doi:10.1145/1671970.1671972.
[2]	O. Kullmann and X. Zhao, “On Davis–Putnam Reductions for Minimally Unsatisfiable Clause-Sets,” Theoretical Computer Science, 492, 2013 pp. 70–87. doi:10.1007/978-3-642-31612-8_ 21.
[3]	R. Aharoni and N. Linial, “Minimal Non-Two-Colorable Hypergraphs and Minimal Unsatisfiable Formulas,” Journal of Combinatorial Theory, Series A 43(2), 1986 pp. 196–204. doi:10.1016/0097-3165(86)90060-9.
[4]	R.Cowen, M. Huq and W. MacDonald, “Implementing the Davis–Putnam Algorithm in Mathematica,” Mathematica in Education and Research, 10, 2005 pp, 46–55. www.researchgate.net/publication/246429822_Implementing_the_Davis-Putnam_Algorithm_in_Mathematica.
[5]	Wikipedia. “Derangement.” (Jul 10, 2010) en.wikipedia.org/wiki/Derangement#Limit_of_ratio_of_derangement_to_permutation_as_n_approaches_∞.
R. Cowen, “Generating Minimally Unsatisfiable Conjunctive Normal Forms,” The Mathematica Journal, 2020. https://doi.org/10.3888/tmj.22–4.

About the Author

Robert Cowen is a Professor Emeritus at Queens College, CUNY. His main research interests are logic and combinatorics. He has enjoyed teaching students how to use Mathematica to do research in mathematics for many years.

Robert Cowen
16422 75th Avenue
Fresh Meadows, NY 11366
robert.cowen@gmail.com