License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.SAT.2023.7
URN: urn:nbn:de:0030-drops-184696
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18469/
Go to the corresponding LIPIcs Volume Portal

de Colnet, Alexis

Separating Incremental and Non-Incremental Bottom-Up Compilation

pdf-format:
LIPIcs-SAT-2023-7.pdf (0.8 MB)

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.

BibTeX - Entry

@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/opus/volltexte/2023/18469},
  URN =		{urn:nbn:de:0030-drops-184696},
  doi =		{10.4230/LIPIcs.SAT.2023.7},
  annote =	{Keywords: Knowledge Compilation, Bottom-up Compilation, DNNF, OBDD}
}

Keywords: Knowledge Compilation, Bottom-up Compilation, DNNF, OBDD
Collection: 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)
Issue Date: 2023
Date of publication: 09.08.2023

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI