Skip to main content
SpringerLink
Log in

Parameterized Compilation Lower Bounds for Restricted CNF-Formulas

  • Conference paper
  • First Online:
Theory and Applications of Satisfiability Testing – SAT 2016 (SAT 2016)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9710))

  • 1948 Accesses

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^{\varOmega (k)}\), and

  • there are CNF formulas of size n and incidence neighborhood diversity k whose smallest DNNF-encoding has size \(n^{\varOmega (\sqrt{k})}\).

These results complement recent upper bounds for compiling CNF into DNNF and strengthen—quantitatively and qualitatively—known conditional lower bounds for cliquewidth. Moreover, they show that, unlike for many graph problems, the parameters considered here behave significantly differently from treewidth.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Note that the definition in [19] differs from the one we give here, but can easily be seen to be equivalent for bipartite graphs and thus incidence graphs of CNF formulas. We keep our definition to be more consistent with the definition of neighborhood diversity.

References

  1. Bova, S., Capelli, F., Mengel, S., Slivovsky, F.: On compiling CNFs into structured deterministic DNNFs. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 199–214. Springer, Heidelberg (2015). doi:10.1007/978-3-319-24318-4_15

    Chapter  Google Scholar 

  2. Bova, S., Capelli, F., Mengel, S., Slivovsky, F.: Knowledge compilation meets communication complexity. In: Proceedings of the 25th International Joint Conference on Artificial Intelligence, IJCAI 2016. IJCAI/AAAI (to appear, 2016)

    Google Scholar 

  3. Brault-Baron, J., Capelli, F., Mengel, S.: Understanding model counting for beta-acyclic CNF-formulas. In: Mayr, E.W., Ollinger, N. (eds.) 32nd International Symposium on Theoretical Aspects of Computer Science, STACS 2015, Garching, Germany, 4–7 March 2015. LIPIcs, vol. 30, pp. 143–156. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)

    Google Scholar 

  4. Chen, H.: Parameterized compilability. In: Kaelbling, L.P., Saffiotti, A. (eds.) Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, IJCAI 2005, Edinburgh, Scotland, UK, 30 July–5 August 2005, pp. 412–417. Professional Book Center (2005)

    Google Scholar 

  5. Chen, H.: Parameter compilation. In: Husfeldt, T., Kanj, I.A. (eds.) 10th International Symposium on Parameterized and Exact Computation, IPEC 2015, Patras, Greece, 16–18 September 2015. LIPIcs, vol. 43, pp. 127–137. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)

    Google Scholar 

  6. Darwiche, A.: Decomposable negation normal form. J. ACM 48(4), 608–647 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  7. Darwiche, A.: New advances in compiling CNF into decomposable negation normal form. In López de Mántaras, R., Saitta, L. (eds.) Proceedings of the 16th Eureopean Conference on Artificial Intelligence, ECAI 2004, including Prestigious Applicants of Intelligent Systems, PAIS 2004, Valencia, Spain, 22–27 August 2004, pp. 328–332. IOS Press (2004)

    Google Scholar 

  8. Darwiche, A., Marquis, P.: A knowledge compilation map. J. Artif. Intell. Res. (JAIR) 17, 229–264 (2002)

    MathSciNet  MATH  Google Scholar 

  9. de Haan, R.: An overview of non-uniform parameterized complexity. Electron. Colloquium Comput. Complex. (ECCC) 22, 130 (2015)

    Google Scholar 

  10. Dell, H., Kim, E.J., Lampis, M., Mitsou, V., Mömke, T.: Complexity and approximability of parameterized MAX-CSPs. In: Husfeldt, T., Kanj, I.A. (eds.) 10th International Symposium on Parameterized and Exact Computation, IPEC 2015, Patras, Greece, 16–18 September 2015. LIPIcs, vol. 43, pp. 294–306. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)

    Google Scholar 

  11. Diestel, R.: Graph Theory. Graduate Texts in Mathematics, vol. 173, 4th edn. Springer, Heidelberg (2012)

    MATH  Google Scholar 

  12. Duris, P., Hromkovic, J., Jukna, S., Sauerhoff, M., Schnitger, G.: On multi-partition communication complexity. Inf. Comput. 194(1), 49–75 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  13. Flum, J., Grohe, M.: Parameterized Complexity Theory. Texts in Theoretical Computer Science. An EATCS Series. Springer, Berlin (2006)

    MATH  Google Scholar 

  14. Huang, J., Darwiche, A.: DPLL with a trace: from SAT to knowledge compilation. In: Kaelbling, L.P., Saffiotti, A. (eds.) Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, IJCAI 2005, Edinburgh, Scotland, UK, 30 July–5 August 2005, pp. 156–162. Professional Book Center (2005)

    Google Scholar 

  15. Koriche, F., Lagniez, J.-M., Marquis, P., Thomas, S.: Compilation, knowledge compilation for model counting : affine decision trees. In Rossi, R. (ed.) Proceedings of the 23rd International Joint Conference on Artificial Intelligence, IJCAI 2013, Beijing, China, 3–9 August 2013. IJCAI/AAAI (2013)

    Google Scholar 

  16. Lampis, M.: Algorithmic meta-theorems for restrictions of treewidth. In: de Berg, M., Meyer, U. (eds.) ESA 2010, Part I. LNCS, vol. 6346, pp. 549–560. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  17. Muise, C., McIlraith, S.A., Beck, J.C., Hsu, E.I.: Dsharp: Fast d-DNNF Compilation with \(\sf sharpSAT\). In: Kosseim, L., Inkpen, D. (eds.) Canadian AI 2012. LNCS, vol. 7310, pp. 356–361. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  18. Ordyniak, S., Paulusma, D., Szeider, S.: Satisfiability of acyclic and almost acyclic CNF formulas. Theor. Comput. Sci. 481, 85–99 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  19. Paulusma, D., Slivovsky, F., Szeider, S.: Model counting for CNF formulas of bounded modular treewidth. In: Portier, N., Wilke, T. (eds.) 30th International Symposium on Theoretical Aspects of Computer Science, STACS 2013, Kiel, Germany, 27 February–2 March 2013. LIPIcs, vol. 20, pp. 55–66. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2013)

    Google Scholar 

  20. Razgon, I.: No small nondeterministic read-once branching programs for CNFs of bounded treewidth. In: Cygan, M., Heggernes, P. (eds.) IPEC 2014. LNCS, vol. 8894, pp. 319–331. Springer, Heidelberg (2014)

    Google Scholar 

  21. Razgon, I.: On OBDDs for CNFs of bounded treewidth. In: Baral, C., De Giacomo, G., Eiter, T. (eds.) Principles of Knowledge Representation and Reasoning: Proceedings of the Fourteenth International Conference, KR 2014, Vienna, Austria, 20–24 July 2014. AAAI Press (2014)

    Google Scholar 

  22. Sæther, S.H., Telle, J.A.: Between treewidth and clique-width. In: Kratsch, D., Todinca, I. (eds.) WG 2014. LNCS, vol. 8747, pp. 396–407. Springer, Heidelberg (2014)

    Google Scholar 

  23. Sang, T., Bacchus, F., Beame, P., Kautz, H.A., Pitassi, T.: Combining component caching and clause learning for effective model counting. In: Proceedings of the Seventh International Conference on Theory and Applications of Satisfiability Testing, SAT 2004, Vancouver, BC, Canada, 10–13 May 2004

    Google Scholar 

  24. Thurley, M.: sharpSAT – counting models with advanced component caching and implicit BCP. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 424–429. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

Download references

Acknowledgments

The author would like to thank Florent Capelli for helpful discussions. Moreover, he thanks Jean-Marie Lagniez for helpful discussions and for experiments with the compiler from [15].

Author information

Authors and Affiliations

  1. CNRS, CRIL UMR 8188, Lens, France

    Stefan Mengel

Authors
  1. Stefan Mengel
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Stefan Mengel .

Editor information

Editors and Affiliations

  1. Aix-Marseille Université, Marseille, France

    Nadia Creignou

  2. Université d'Artois, Lens, France

    Daniel Le Berre

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Mengel, S. (2016). Parameterized Compilation Lower Bounds for Restricted CNF-Formulas. In: Creignou, N., Le Berre, D. (eds) Theory and Applications of Satisfiability Testing – SAT 2016. SAT 2016. Lecture Notes in Computer Science(), vol 9710. Springer, Cham. https://doi.org/10.1007/978-3-319-40970-2_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-40970-2_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-40969-6

  • Online ISBN: 978-3-319-40970-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation