2015/05/09 by Oliver Kullmann, Kullmann, Oliver, Xishun Zhao +1
Computer Science · Mathematics · #03B05 #05D99 (Secondary) #68R99 (Primary) #Advanced Algebra and Logic #Advanced Mathematical Theories #Combinatorics (math.CO) #Computability, Logic, AI Algorithms #Discrete Mathematics (cs.DM) #F.2.2 #FOS: Computer and information sciences #FOS: Mathematics #G.2.2 #Logic in Computer Science (cs.LO) #acm:03B05 #acm:05D99 #acm:68R99 #cs.DM #cs.LO #math.CO #msc:03B05 #msc:05D99 #msc:68R99
paper · pdf · doi:10.48550/arxiv.1505.02318
19 pages; second version with more explanations and examples
openalex publication_date 2015/05/09 · arxiv created 2015/07/08 · arxiv updated 2015/07/09 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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 S2(k) <= FCM(k), where FCM(k) is the maximal number of full clauses in MUs of deficiency k, while S2(k) is the smallest n such that 2k 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 S2 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 S2(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 S2(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.