Small Unsatisfiable k-CNFs with Bounded Literal Occurrence

Zhang, Tianwei; Peitl, Tomáš; Szeider, Stefan

doi:10.4230/LIPIcs.SAT.2024.31

Record link:

http://hdl.handle.net/20.500.12708/208734

Title:

Small Unsatisfiable k-CNFs with Bounded Literal Occurrence

Citation:

Zhang, T., Peitl, T., & Szeider, S. (2024). Small Unsatisfiable k-CNFs with Bounded Literal Occurrence. In Leibniz International Proceedings in Informatics, LIPIcs (No. 31; pp. 31:1-31:22). Schloss Dagstuhl – Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.SAT.2024.31

CatalogPlus:

AC17409118

Publisher DOI:

10.4230/LIPIcs.SAT.2024.31

Publication Type:

Inproceedings - Full-Paper Contribution

Language:

English

Authors:

Zhang, Tianwei
Peitl, Tomáš
Szeider, Stefan

Organisational Unit:

E192-01 - Forschungsbereich Algorithms and Complexity
E056-13 - Fachbereich LogiCS
E056-23 - Fachbereich Innovative Combinations and Applications of AI and ML (iCAIML)

Published in:

27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

ISBN:

978-3-95977-334-8

Volume:

305

DOI of the book:

10.4230/LIPIcs.SAT.2024.0

Date (published):

2024

Event name:

27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Event date:

21-Aug-2024 - 24-Aug-2024

Event place:

Pune, India

Number of Pages:

Publisher:

Schloss Dagstuhl – Leibniz-Zentrum für Informatik

Peer reviewed:

Yes

Keywords:

(ks)-SAT; k-CNF; minimally unsatisfiable formulas; symmetry breaking

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.

Research Areas:

Logic and Computation: 100%

Science Branch:

1020 - Informatik: 80%
1010 - Mathematik: 20%

License:

CC BY 4.0