arXiv++ Combinatorics

The topic of this paper is the Finiteness Conjecture for minimally unsatisfiable clause-sets (MUs), stating that for each fixed deficiency (number of clauses minus number of variables) there are only finitely many patterns, given a certain basic reduction (generalising unit-clause propagation). We focus our attention on hitting clause-sets (every two clauses have at least one clash), where the conjecture says that there are only finitely many isomorphism types. The Finiteness Conjecture is here known to hold for deficiency at most 2, and we now prove it for deficiency 3. An important tool is the notion of "(ir)reducible clause-sets": we show how to reduce the general question to the irreducible case, and then solve this case (for deficiency 3). This notion comes from number theory (Korec 1984, Berger et al 1990), and we rediscovered it in our studies.

We establish a new bridge between propositional logic and elementary number theory. The main objects are "minimally unsatisfiable clause-sets", short "MUs", unsatisfiable conjunctive normal forms rendered satisfiable by elimination of any clause. In other words, irredundant coverings of the boolean hypercube by subcubes. The main parameter for MUs is the "deficiency" k, the difference between the number of clauses and the number of variables (the difference between the number of elements in the covering and the dimension of the hypercube), and the fundamental fact is that k >= 1 holds. A "full clause" in an MU contains all variables (corresponding to a singleton in the covering). We show the lower bound S_2(k) <= FCM(k), where FCM(k) is the maximal number of full clauses in MUs of deficiency k, while S_2(k) is the smallest n such that 2^k divides n!. The proof rests on two methods: On the logic-combinatorial side, applying subsumption resolution and its inverse, a fundamental method since Boole in 1854 introduced the "expansion method". On the arithmetical side, analysing certain recursions, combining an application-specific recursion with a recursion from the field of meta-Fibonacci sequences (indeed S_2 equals twice the Conolly sequence). A further tool is the consideration of unsatisfiable "hitting clause-sets" (UHITs), special cases of MUs, which correspond to the partitions of the boolean hypercube by subcubes; they are also known as orthogonal or disjoint DNF tautologies. We actually show the sharper lower bound S_2(k) <= FCH(k), where FCH(k) is the maximal number of full clauses in UHITs of deficiency k. We conjecture that for all k holds S_2(k) = FCH(k), which would establish a surprising connection between the extremal combinatorics of (un)satisfiability and elementary number theory. We apply the lower bound to analyse the structure of MUs and UHITs.

We investigate connections between SAT (the propositional satisfiability problem) and combinatorics, around the minimum degree (number of occurrences) of variables in various forms of redundancy-free boolean conjunctive normal forms (clause-sets). Lean clause-sets do not have non-trivial autarkies, that is, it is not possible to satisfy some clauses and leave the other clauses untouched. The deficiency of a clause-set is the difference of the number of clauses and the number of variables. We prove a precise upper bound on the minimum variable degree of lean clause-sets in dependency on the deficiency. If a clause-set does not fulfil this upper bound, then it must have a non-trivial autarky; we show that the autarky-reduction (elimination of affected clauses) can be done in polynomial time, while it is open to find the autarky itself in polynomial time. Then we investigate this upper bound for the special case of minimally unsatisfiable clause-sets. We show that the bound can be improved here, introducing a general method to improve the underlying recurrence. We consider precise relations, and thus the investigations have a number-theoretical flavour. We try to build a bridge from logic to combinatorics (especially to hypergraph colouring), and we discuss thoroughly the background and open problems, and provide many examples and explanations.

For investigations into the structure of MU, i.e., minimally unsatisfiable clause-sets or conjunctive normal forms, singular DP-reduction is a fundamental tool, applying DP-reduction F -> DP_v(F) in case variable v occurs in one polarity only once. Recall, in general DP_v(F) replaces all clauses containing variable v by their resolvents on v (another name is "variable elimination"). We consider sDP(F), the set of all results of applying singular DP-reduction to F in MU as long as possible, obtaining non-singular F' in MU with the same deficiency, i.e., delta(F') = delta(F). (In general, delta(F) is the difference c(F) - n(F) of the number of clauses and the number of variables.) Our main results are: 1. For all F', F" in sDP(F) we have n(F') = n(F"). 2. If F is saturated (F in SMU), then we have |sDP(F)| = 1. 3. If F is "eventually saturated", that is, sDP(F) <= SMU, then for F', F" in sDP(F) we have F' isomorphic F" (establishing "confluence modulo isomorphism"). The results are obtained by a detailed analysis of singular DP-reduction for F in MU. As an application we obtain that singular DP-reduction for F in MU(2) (i.e., delta(F) = 2) is confluent modulo isomorphism (using the fundamental characterisation of MU(2) by Kleine Buening). The background for these considerations is the general project of the classification of MU in terms of the deficiency.

We consider the question of the existence of variables with few occurrences in boolean conjunctive normal forms (clause-sets). Let mvd(F) for a clause-set F denote the minimal variable-degree, the minimum of the number of occurrences of variables. Our main result is an upper bound mvd(F) <= nM(surp(F)) <= surp(F) + 1 + log_2(surp(F)) for lean clause-sets F in dependency on the surplus surp(F). - Lean clause-sets, defined as having no non-trivial autarkies, generalise minimally unsatisfiable clause-sets. - For the surplus we have surp(F) <= delta(F) = c(F) - n(F), using the deficiency delta(F) of clause-sets, the difference between the number of clauses and the number of variables. - nM(k) is the k-th "non-Mersenne" number, skipping in the sequence of natural numbers all numbers of the form 2^n - 1. We conjecture that this bound is nearly precise for minimally unsatisfiable clause-sets. As an application of the upper bound we obtain that (arbitrary!) clause-sets F with mvd(F) > nM(surp(F)) must have a non-trivial autarky (so clauses can be removed satisfiability-equivalently by an assignment satisfying some clauses and not touching the other clauses). It is open whether such an autarky can be found in polynomial time. As a future application we discuss the classification of minimally unsatisfiable clause-sets depending on the deficiency.