Parameterized compilation lower bounds for restricted CNF-formulas

DOI10.1007/978-3-319-40970-2_1MaRDI QIDQ2817997zbMATH OpenOpenAlexFDO

Authors Stefan Mengel

Publication date 5 September 2016

Published in Theory and Applications of Satisfiability Testing – SAT 2016 (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1604.06715

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Computational aspects of satisfiability (68R07) Graph theory (including graph drawing) in computer science (68R10)

Abstract: We show unconditional parameterized lower bounds in the area of knowledge compilation, more specifically on the size of circuits in decomposable negation normal form (DNNF) that encode CNF-formulas restricted by several graph width measures. In particular, we show that - there are CNF formulas of size $n$ and modular incidence treewidth $k$ whose smallest DNNF-encoding has size $n^{Omega(k)}$, and - there are CNF formulas of size $n$ and incidence neighborhood diversity $k$ whose smallest DNNF-encoding has size $n^{Omega(sqrtk)}$. These results complement recent upper bounds for compiling CNF into DNNF and strengthen---quantitatively and qualitatively---known conditional low-er bounds for cliquewidth. Moreover, they show that, unlike for many graph problems, the parameters considered here behave significantly differently from treewidth.

Recommendations

• Connecting knowledge compilation classes and width parameters
• On compiling CNFs into structured deterministic DNNFs
• Connecting width and structure in knowledge compilation
• CV-width: a new complexity parameter for CNFs
• Revisiting graph width measures for CNF-encodings

Cites work

• Algorithmic meta-theorems for restrictions of treewidth
• Between treewidth and clique-width
• Complexity and Approximability of Parameterized MAX-CSPs
• Decomposable negation normal form
• scientific article; zbMATH DE number 1946853 (Why is no real title available?)
• scientific article; zbMATH DE number 1518742 (Why is no real title available?)
• Model counting for CNF formulas of bounded modular treewidth
• No small nondeterministic read-once branching programs for CNFs of bounded treewidth
• On compiling CNFs into structured deterministic DNNFs
• On multi-partition communication complexity
• Parameter compilation
• Satisfiability of acyclic and almost acyclic CNF formulas
• Understanding model counting for -acyclic CNF-formulas

Cited in

(15)

• Revisiting graph width measures for CNF-encodings
• Connecting width and structure in knowledge compilation
• On compiling CNFs into structured deterministic DNNFs
• Fixed parameter tractable optimization under DNNF constraints
• Finer tight bounds for coloring on clique-width
• Graph width measures for CNF-encodings with auxiliary variables
• Finer tight bounds for coloring on clique-width
• CV-width: a new complexity parameter for CNFs
• Cliquewidth and knowledge compilation
• Functional Treewidth: Bounding Complexity in the Presence of Functional Dependencies
• Non-finite axiomatisability results via reductions: CSP parallel composition and CCS restriction
• Tight Algorithms for Connectivity Problems Parameterized by Modular-Treewidth
• An Abstract CNF-to-d-DNNF Compiler Based on Chronological CDCL
• Towards exact structural thresholds for parameterized complexity
• Bridging treewidth and clique-width via cograph-modular-treewidth

Describes a project that uses

Uses Software

• sharpSAT
• Dsharp

This page was built for publication: Parameterized compilation lower bounds for restricted CNF-formulas

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2817997)