Small unsatisfiable $k$-CNFs with bounded literal occurrence

TL;DR

This paper identifies the smallest unsatisfiable $k$-CNF formulas with bounded literals, improving bounds for specific subclasses and using a novel combination of theoretical and computational methods.

Contribution

It determines the smallest unsatisfiable formulas in certain $k$-CNF subclasses and introduces an efficient graph encoding for symmetry-breaking SAT searches.

Findings

Smallest unsatisfiable formulas for 3-CNF subclasses are fully characterized.

Reduced size of known unsatisfiable formulas for 4-CNF with limited variable occurrences.

Combined theoretical and computational approach enhances formula size bounds.

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.