We establish a new bridge between propositional logic and elementary number theory. A full clause in a conjunctive normal form (CNF) contains all variables, and we study them in minimally unsatisfiable clause-sets (MU); such clauses are strong structural anchors, when combined with other restrictions. Counting the maximal number of full clauses for a given deficiency k, we obtain a close connection to the so-called “Smarandache primitive number” S2(k), the smallest n such that 2 k divides n!. The deficiency k � 1 of an MU is the difference between the number of clauses and the number of variables. We also consider the subclass UHIT of MU given by unsatisfiable hitting clause-sets, where every two clauses clash. While MU corresponds to irredundant (minimal) covers of the boolean hypercube {0,1} n by sub-cubes, for UHIT the covers must indeed be partitions. We study the four fundamental quantities FCH,FCM,VDH,VDM : N ! N, defined as the maximum number of full clauses in UHIT resp. MU, resp. the maximal minimal number of occurrences of a variable (the variable degree) in UHIT resp. MU, in dependency on the deficiency. We have the relations FCH(k) � FCM(k) � VDM(k) and FCH(k) � VDH(k) � VDM(k), together with VDM(k) � nM(k) � k + 1 + log2(k), for the “non-Mersenne numbers” nM(k), enumerating the natural numbers except numbers of the form 2 n 1. We show the lower bound S2(k) � FCH(k); indeed we conjecture this to be exact. The proof rests on two methods: Applying an expansion process, fundamental since the days of Boole, and analysing certain recursions, combining an application-specific recursion with a recursion from the field of meta-Fibonacci sequences. The S2-lower bound together with the nM-upper-bound yields a good handle on the four fundamental quantities, especially for those k with S2(k) = nM(k) (we show there are infinitely many such k), since then the four quantities must all be equal to S2(k) = nM(k). With the help of this we determine them for 1 � k � 13.
['Oliver Kullmann', 'Xishun Zhao']
Parameters for minimal unsatisfiability: Smarandache primitive numbers and full clauses