Abstract
Knowledge compilation is a compelling technique for dealing with the intractability of propositional reasoning. One particularly effective target language is Deterministic Decomposable Negation Normal Form (d-DNNF). We exploit recent advances in #SAT solving in order to produce a new state-of-the-art CNF → d-DNNF compiler: Dsharp. Empirical results demonstrate that Dsharp is generally an order of magnitude faster than c2d, the de facto standard for compiling to d-DNNF, while yielding a representation of comparable size.
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
Beame, P., Kautz, H., Sabharwal, A.: Understanding the power of clause learning. In: International Joint Conference on Artificial Intelligence, vol. 18, pp. 1194–1201 (2003)
Chavira, M., Darwiche, A., Jaeger, M.: Compiling relational bayesian networks for exact inference. International Journal of Approximate Reasoning 42, 4–20 (2006)
Darwiche, A., Marquis, P.: A knowledge compilation map. Journal of Artificial Intelligence Research 17, 229–264 (2002)
Darwiche, A.: New advances in compiling CNF to decomposable negational normal form. In: Proceedings of European Conference on Artificial Intelligence (2004)
Huang, J., Darwiche, A.: DPLL with a trace: from SAT to knowledge compilation. In: International Joint Conference On Artificial Intelligence, pp. 156–162 (2005)
Jha, A., Suciu, D.: Knowledge compilation meets database theory: compiling queries to decision diagrams. In: Proceedings of the 14th International Conference on Database Theory, pp. 162–173. ACM (2011)
Muise, C., McIlraith, S.A., Beck, J.C., Hsu, E.: Fast d-DNNF compilation with sharpSAT. In: Workshop on Abstraction, Reformulation, and Approximation, AAAI 2010 (2010)
Palacios, H., Bonet, B., Darwiche, A., Geffner, H.: Pruning conformant plans by counting models on compiled d-DNNF representations. In: Proceedings of the 15th International Conference on Automated Planning and Scheduling, pp. 141–150 (2005)
Siddiqi, S., Huang, J.: Probabilistic sequential diagnosis by compilation. In: Tenth International Symposium on Artificial Intelligence and Mathematics (2008)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Muise, C., McIlraith, S.A., Beck, J.C., Hsu, E.I. (2012). Dsharp: Fast d-DNNF Compilation with sharpSAT . In: Kosseim, L., Inkpen, D. (eds) Advances in Artificial Intelligence. Canadian AI 2012. Lecture Notes in Computer Science(), vol 7310. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30353-1_36
Download citation
DOI: https://doi.org/10.1007/978-3-642-30353-1_36
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-30352-4
Online ISBN: 978-3-642-30353-1
eBook Packages: Computer ScienceComputer Science (R0)