Abstract
We show that the traces of recently introduced dynamic programming algorithms for #SAT can be used to construct structured deterministic DNNF (decomposable negation normal form) representations of propositional formulas in CNF (conjunctive normal form). This allows us prove new upper bounds on the complexity of compiling CNF formulas into structured deterministic DNNFs in terms of parameters such as the treewidth and the clique-width of the incidence graph.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bova, S., Capelli, F., Mengel, S., Slivovsky, F.: Expander CNFs have exponential DNNF size. CoRR, abs/1411.1995 (2014)
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. LIPIcs, vol. 30, pp. 143–156. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)
Chen, H.: Parameterized compilability. In: Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, IJCAI 2005, Edinburgh, Scotland, UK, July 30-August 5, 2005, pp. 412–417 (2005)
Darwiche, A.: Decomposable negation normal form. J. ACM 48(4), 608–647 (2001)
Darwiche, A.: On the tractable counting of theory models and its application to truth maintenance and belief revision. Journal of Applied Non-Classical Logics 11(1–2), 11–34 (2001)
Darwiche, A., Marquis, P.: A Knowledge Compilation Map. J. Artif. Intell. Res. (JAIR) 17, 229–264 (2002)
Flum, J., Grohe, M.: Parameterized Complexity Theory. Springer-Verlag, New York (2006)
Hlinený, P., Oum, S., Seese, D., Gottlob, G.: Width parameters beyond tree-width and their applications. Comput. J. 51(3), 326–362 (2008)
Karp, R.M., Lipton, R.J.: Some connections between nonuniform and uniform complexity classes. In: Proceedings of STOC 1980, pp. 302–309. ACM (1980)
Ordyniak, S., Paulusma, D., Szeider, S.: Satisfiability of acyclic and almost acyclic CNF formulas. Theoretical Computer Science 481, 85–99 (2013)
Oztok, U., Darwiche, A.: CV-width: a new complexity parameter for CNFs. In: 21st European Conference on Artificial Intelligence, ECAI 2014, pp. 675–680 (2014)
Oztok, U., Darwiche, A.: On compiling CNF into decision-DNNF. In: O’Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 42–57. Springer, Heidelberg (2014)
Pipatsrisawat, K., Darwiche, A.: New compilation languages based on structured decomposability. In: Proceedings of the 23rd National Conference on Artificial Intelligence, AAAI 2008, vol. 1, pp. 517–522. AAAI Press (2008)
Pipatsrisawat, K., Darwiche, A.: Top-down algorithms for constructing structured DNNF: theoretical and practical implications. In: Proceedings of 19th European Conference on Artificial Intelligence, ECAI 2010, Lisbon, Portugal, August 16–20, 2010. Frontiers in Artificial Intelligence and Applications, vol. 215, pp. 3–8. IOS Press (2010)
Razgon, I., Petke, J.: Cliquewidth and knowledge compilation. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 335–350. Springer, Heidelberg (2013)
Sæther, S.H., Telle, J.A., Vatshelle, M.: Solving MaxSAT and #SAT on structured CNF formulas. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 16–31. Springer, Heidelberg (2014)
Slivovsky, F., Szeider, S.: Model counting for formulas of bounded Clique-Width. In: Cai, L., Cheng, S.-W., Lam, T.-W. (eds.) Algorithms and Computation. LNCS, vol. 8283, pp. 677–687. Springer, Heidelberg (2013)
Vatshelle, M.: New Width Parameters of Graphs. PhD thesis, University of Bergen (2012)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Bova, S., Capelli, F., Mengel, S., Slivovsky, F. (2015). On Compiling CNFs into Structured Deterministic DNNFs. In: Heule, M., Weaver, S. (eds) Theory and Applications of Satisfiability Testing -- SAT 2015. SAT 2015. Lecture Notes in Computer Science(), vol 9340. Springer, Cham. https://doi.org/10.1007/978-3-319-24318-4_15
Download citation
DOI: https://doi.org/10.1007/978-3-319-24318-4_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-24317-7
Online ISBN: 978-3-319-24318-4
eBook Packages: Computer ScienceComputer Science (R0)