DROPS

Document

DOI: 10.4230/LIPIcs.SAT.2022.9

A Generalization of the Satisfiability Coding Lemma and Its Applications

Authors: Milan Mossé, Harry Sha, and Li-Yang Tan

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)

Abstract

The seminal Satisfiability Coding Lemma of Paturi, Pudlák, and Zane is a coding scheme for satisfying assignments of k-CNF formulas. We generalize it to give a coding scheme for implicants and use this generalized scheme to establish new structural and algorithmic properties of prime implicants of k-CNF formulas. Our first application is a near-optimal bound of n⋅ 3^{n(1-Ω(1/k))} on the number of prime implicants of any n-variable k-CNF formula. This resolves an open problem from the Ph.D. thesis of Talebanfard, who proved such a bound for the special case of constant-read k-CNF formulas. Our proof is algorithmic in nature, yielding an algorithm for computing the set of all prime implicants - the Blake Canonical Form - of a given k-CNF formula. The problem of computing the Blake Canonical Form of a given function is a classic one, dating back to Quine, and our work gives the first non-trivial algorithm for k-CNF formulas.

Cite as

Milan Mossé, Harry Sha, and Li-Yang Tan. A Generalization of the Satisfiability Coding Lemma and Its Applications. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{mosse_et_al:LIPIcs.SAT.2022.9,
  author =	{Moss\'{e}, Milan and Sha, Harry and Tan, Li-Yang},
  title =	{{A Generalization of the Satisfiability Coding Lemma and Its Applications}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{9:1--9:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.9},
  URN =		{urn:nbn:de:0030-drops-166837},
  doi =		{10.4230/LIPIcs.SAT.2022.9},
  annote =	{Keywords: Prime Implicants, Satisfiability Coding Lemma, Blake Canonical Form, k-SAT}
}

Search Results

Documents authored by Sha, Harry

A Generalization of the Satisfiability Coding Lemma and Its Applications

Abstract

Cite as

Thanks for your feedback!

Could not send message