Small unsatisfiable $k$-CNFs with bounded literal occurrence
Abstract
We obtain the smallest unsatisfiable formulas in subclasses of -CNF (exactly 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.
Keywords
Cite
@article{arxiv.2405.16149,
title = {Small unsatisfiable $k$-CNFs with bounded literal occurrence},
author = {Tianwei Zhang and Tomáš Peitl and Stefan Szeider},
journal= {arXiv preprint arXiv:2405.16149},
year = {2024}
}
Comments
full version of a paper to appear in the proceedings of SAT 2024, slight revision compared to v1