DROPS

Document

DOI: 10.4230/LIPIcs.SAT.2024.31

Small Unsatisfiable k-CNFs with Bounded Literal Occurrence

Authors: Tianwei Zhang, Tomáš Peitl, and Stefan Szeider

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

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.

Cite as

Tianwei Zhang, Tomáš Peitl, and Stefan Szeider. Small Unsatisfiable k-CNFs with Bounded Literal Occurrence. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 31:1-31:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{zhang_et_al:LIPIcs.SAT.2024.31,
  author =	{Zhang, Tianwei and Peitl, Tom\'{a}\v{s} and Szeider, Stefan},
  title =	{{Small Unsatisfiable k-CNFs with Bounded Literal Occurrence}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{31:1--31:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.31},
  URN =		{urn:nbn:de:0030-drops-205531},
  doi =		{10.4230/LIPIcs.SAT.2024.31},
  annote =	{Keywords: k-CNF, (k,s)-SAT, minimally unsatisfiable formulas, symmetry breaking}
}

Document

DOI: 10.4230/LIPIcs.CP.2023.39

Searching for Smallest Universal Graphs and Tournaments with SAT

Authors: Tianwei Zhang and Stefan Szeider

Published in: LIPIcs, Volume 280, 29th International Conference on Principles and Practice of Constraint Programming (CP 2023)

Abstract

A graph is induced k-universal if it contains all graphs of order k as an induced subgraph. For over half a century, the question of determining smallest k-universal graphs has been studied. A related question asks for a smallest k-universal tournament containing all tournaments of order k. This paper proposes and compares SAT-based methods for answering these questions exactly for small values of k. Our methods scale to values for which a generate-and-test approach isn't feasible; for instance, we show that an induced 7-universal graph has more than 16 vertices, whereas the number of all connected graphs on 16 vertices, modulo isomorphism, is a number with 23 decimal digits Our methods include static and dynamic symmetry breaking and lazy encodings, employing external subgraph isomorphism testing.

Cite as

Tianwei Zhang and Stefan Szeider. Searching for Smallest Universal Graphs and Tournaments with SAT. In 29th International Conference on Principles and Practice of Constraint Programming (CP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 280, pp. 39:1-39:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{zhang_et_al:LIPIcs.CP.2023.39,
  author =	{Zhang, Tianwei and Szeider, Stefan},
  title =	{{Searching for Smallest Universal Graphs and Tournaments with SAT}},
  booktitle =	{29th International Conference on Principles and Practice of Constraint Programming (CP 2023)},
  pages =	{39:1--39:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-300-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{280},
  editor =	{Yap, Roland H. C.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2023.39},
  URN =		{urn:nbn:de:0030-drops-190760},
  doi =		{10.4230/LIPIcs.CP.2023.39},
  annote =	{Keywords: Constrained-based combinatorics, synthesis problems, symmetry breaking, SAT solving, subgraph isomorphism, tournament, directed graphs}
}

Search Results

Documents authored by Zhang, Tianwei

Small Unsatisfiable k-CNFs with Bounded Literal Occurrence

Abstract

Cite as

Searching for Smallest Universal Graphs and Tournaments with SAT

Abstract

Cite as

Thanks for your feedback!

Could not send message