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. © 2012 Springer-Verlag.
Cite
CITATION STYLE
Muise, C., McIlraith, S. A., Beck, J. C., & Hsu, E. I. (2012). DSHARP: Fast d-DNNF compilation with sharpSAT. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7310 LNAI, pp. 356–361). https://doi.org/10.1007/978-3-642-30353-1_36
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
