Skip to main content
SpringerLink
Log in
Book cover

International Conference on Principles and Practice of Constraint Programming

CP 2014: Principles and Practice of Constraint Programming pp 42–57Cite as

On Compiling CNF into Decision-DNNF

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 8656))

Abstract

Decision-DNNF is a strict subset of decomposable negation normal form (DNNF) that plays a key role in analyzing the complexity of model counters (the searches performed by these counters have their traces in Decision-DNNF). This paper presents a number of results on Decision-DNNF. First, we introduce a new notion of CNF width and provide an algorithm that compiles CNFs into Decision-DNNFs in time and space that are exponential only in this width. The new width strictly dominates the treewidth of the CNF primal graph: it is no greater and can be bounded when the treewidth of the primal graph is unbounded. This new result leads to a tighter bound on the complexity of model counting. Second, we show that the output of the algorithm can be converted in linear time to a sentential decision diagram (SDD), which leads to a tighter bound on the complexity of compiling CNFs into SDDs.

This is a preview of subscription content, 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   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bacchus, F., Dalmao, S., Pitassi, T.: DPLL with Caching: A new algorithm for #SAT and Bayesian Inference. In: Electronic Colloquium on Computational Complexity (ECCC), vol. 10(003) (2003)

    Google Scholar 

  2. Beame, P., Li, J., Roy, S., Suciu, D.: Lower Bounds for Exact Model Counting and Applications in Probabilistic Databases. In: Proc. of UAI (2013)

    Google Scholar 

  3. Blum, M., Chandra, A.K., Wegman, M.N.: Equivalence of free boolean graphs can be decided probabilistically in polynomial time. Inf. Process. Lett. 10(2), 80–82 (1980)

    Article  MATH  MathSciNet  Google Scholar 

  4. Bryant, R.E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. Computers 35(8), 677–691 (1986)

    Article  MATH  Google Scholar 

  5. Chavira, M., Darwiche, A.: On Probabilistic Inference by Weighted Model Counting. Artif. Intell. 172(6-7), 772–799 (2008)

    Article  MATH  MathSciNet  Google Scholar 

  6. Darwiche, A.: Decomposable Negation Normal Form. J. ACM 48(4), 608–647 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  7. Darwiche, A.: New Advances in Compiling CNF into Decomposable Negation Normal Form. In: Proc. of ECAI, pp. 328–332 (2004)

    Google Scholar 

  8. Darwiche, A.: SDD: A New Canonical Representation of Propositional Knowledge Bases. In: Proc. of IJCAI, pp. 819–826 (2011)

    Google Scholar 

  9. Darwiche, A., Marquis, P.: A Knowledge Compilation Map. J. Artif. Intell. Res. (JAIR) 17, 229–264 (2002)

    Google Scholar 

  10. Davis, M., Logemann, G., Loveland, D.W.: A Machine Program for Theorem-Proving. Commun. ACM 5(7), 394–397 (1962)

    Article  MATH  MathSciNet  Google Scholar 

  11. Davis, M., Putnam, H.: A Computing Procedure for Quantification Theory. J. ACM 7(3), 201–215 (1960)

    Article  MATH  MathSciNet  Google Scholar 

  12. Huang, J., Darwiche, A.: The Language of Search. J. Artif. Intell. Res. (JAIR) 29, 191–219 (2007)

    Google Scholar 

  13. Bayardo Jr., R.J., Pehoushek, J.D.: Counting Models Using Connected Components. In: AAAI/IAAI, pp. 157–162 (2000)

    Google Scholar 

  14. Majercik, S.M., Littman, M.L.: Using Caching to Solve Larger Probabilistic Planning Problems. In: AAAI/IAAI, pp. 954–959 (1998)

    Google Scholar 

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

    Chapter  Google Scholar 

  16. Oztok, U., Darwiche, A.: CV-width: A New Complexity Parameter for CNFs. In: Proc. of ECAI (to appear, 2014)

    Google Scholar 

  17. Pipatsrisawat, K., Darwiche, A.: A Lower Bound on the Size of Decomposable Negation Normal Form. In: Proc. of AAAI (2010)

    Google Scholar 

  18. Pipatsrisawat, K., Darwiche, A.: Top-Down Algorithms for Constructing Structured DNNF: Theoretical and Practical Implications. In: Proc. of ECAI. pp. 3–8 (2010)

    Google Scholar 

  19. Robertson, N., Seymour, P.D.: Graph minors. III. Planar tree-width. J. Comb. Theory, Ser. B 36(1), 49–64 (1984)

    Article  MATH  MathSciNet  Google Scholar 

  20. Sang, T., Bacchus, F., Beame, P., Kautz, H.A., Pitassi, T.: Combining Component Caching and Clause Learning for Effective Model Counting. In: Proc. of SAT (2004)

    Google Scholar 

  21. Valiant, L.G.: The complexity of computing the permanent. Theor. Comput. Sci. 8, 189–201 (1979)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, University of California, Los Angeles, CA, 90095, USA

    Umut Oztok & Adnan Darwiche

Authors
  1. Umut Oztok
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Adnan Darwiche
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Insight Centre for Data Analytics, School of Computer Science and IT, University College Cork, Western Road, Cork, Ireland

    Barry O’Sullivan

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Oztok, U., Darwiche, A. (2014). On Compiling CNF into Decision-DNNF. In: O’Sullivan, B. (eds) Principles and Practice of Constraint Programming. CP 2014. Lecture Notes in Computer Science, vol 8656. Springer, Cham. https://doi.org/10.1007/978-3-319-10428-7_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-10428-7_7

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-10427-0

  • Online ISBN: 978-3-319-10428-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation