Small unsatisfiable $k$-CNFs with bounded literal occurrence

TL;DR

This work investigates the smallest unsatisfiable formulas in subclasses of $k$-CNF with bounded literal occurrences, with a focus on $(k,s)$- and $(k,p,q)$-formulas in the 3- and 4-CNF regimes. It introduces a robust SMS-based, isomorph-free search framework and a graph-based encoding to systematically enumerate candidate formulas, achieving exact values for many small $(3,s)$ and $(3,p,q)$ cases and a new record of 235 clauses for a unsatisfiable $(4,5)$-formula. Key methodological advances include hard-coding parts of the clause-literal matrix, disjunctive splitting, stairway-based reasoning, and reductions that together produce tight lower and upper bounds, plus a dichotomy for $(3,1,q)$-SAT. These results sharpen inapproximability implications for MaxSAT within bounded-occurrence CNF classes and demonstrate the practical utility of SMS for combinatorial formula discovery and verification.

Abstract

We obtain the smallest unsatisfiable formulas in subclasses of $k$-CNF (exactly $k$ distinct literals per clause) with bounded variable or literal occurrences. Smaller unsatisfiable formulas of this type translate into stronger inapproximability results for MaxSAT in the considered formula class. Our results cover subclasses of 3-CNF and 4-CNF; in all subclasses of 3-CNF we considered we were able to determine the smallest size of an unsatisfiable formula; in the case of 4-CNF with at most 5 occurrences per variable we decreased the size of the smallest known unsatisfiable formula. Our methods combine theoretical arguments and symmetry-breaking exhaustive search based on SAT Modulo Symmetries (SMS), a recent framework for isomorph-free SAT-based graph generation. To this end, and as a standalone result of independent interest, we show how to encode formulas as graphs efficiently for SMS.

Figures (3)

• Figure 1: Consider the formula $F=\{C_1,C_2,C_3\}$ with $C_1=\{x,y\}$, $C_2=\{x,\overline{y}\}$, and $C_3=\{\overline{x}\}$. We see the corresponding 2-graph and the upper part of its lexicographically minimal adjacency matrix. Observe how the left part is indeed antidiagonal.
• Figure 2: The first rows of the matrix determined as a result of our choice for $\text{\normalfont pos}(i)$ and $\text{\normalfont neg}(i)$. The omitted values are all $0$.
• Figure 3: The $\oplus$- derivation of Knuth's formula $K_{4,5}$. Each node has two incoming arcs; the number of arrowheads denotes the values $p,q$ in $\oplus_{p,q}$.

Theorems & Definitions (28)

• Theorem 1
• proof
• Lemma 2
• proof
• Lemma 3
• proof
• Lemma 4
• proof
• Theorem 5: Dichotomy
• proof