Search Results

Documents authored by de Colnet, Alexis

Document
DOI: 10.4230/LIPIcs.SAT.2023.7
Separating Incremental and Non-Incremental Bottom-Up Compilation

Authors: Alexis de Colnet

Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)

Abstract
The aim of a compiler is, given a function represented in some language, to generate an equivalent representation in a target language L. In bottom-up (BU) compilation of functions given as CNF formulas, constructing the new representation requires compiling several subformulas in L. The compiler starts by compiling the clauses in L and iteratively constructs representations for new subformulas using an "Apply" operator that performs conjunction in L, until all clauses are combined into one representation. In principle, BU compilation can generate representations for any subformulas and conjoin them in any way. But an attractive strategy from a practical point of view is to augment one main representation - which we call the core - by conjoining to it the clauses one at a time. We refer to this strategy as incremental BU compilation. We prove that, for known relevant languages L for BU compilation, there is a class of CNF formulas that admit BU compilations to L that generate only polynomial-size intermediate representations, while their incremental BU compilations all generate an exponential-size core.
Cite as

Alexis de Colnet. Separating Incremental and Non-Incremental Bottom-Up Compilation. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 7:1-7:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{decolnet:LIPIcs.SAT.2023.7,
  author =	{de Colnet, Alexis},
  title =	{{Separating Incremental and Non-Incremental Bottom-Up Compilation}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{7:1--7:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.7},
  URN =		{urn:nbn:de:0030-drops-184696},
  doi =		{10.4230/LIPIcs.SAT.2023.7},
  annote =	{Keywords: Knowledge Compilation, Bottom-up Compilation, DNNF, OBDD}
}
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact