1 Search Results for "Sha, Harry"

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-dev.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}
}
  • Refine by Author
  • 1 Mossé, Milan
  • 1 Sha, Harry
  • 1 Tan, Li-Yang

  • Refine by Classification
  • 1 Theory of computation

  • Refine by Keyword
  • 1 Blake Canonical Form
  • 1 Prime Implicants
  • 1 Satisfiability Coding Lemma
  • 1 k-SAT

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2022

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact