DSHARP -- CNF-to-dDNNF Compiler

Welcome to the DSHARP Website

DSHARP is an open source CNF-to-dDNNF compiler based on sharpSAT. Similar to the c2d software, DSHARP takes a boolean theory in conjunctive normal form as input, and compiles it into deterministic decomposable negation normal form.

This paper describes the DSHARP system, and further information on the approach can be found in an extended version [here].

If you would like to contribute to DSHARP, or have any questions regarding its usage, you can find my contact info [here]. You can also issue a specific bug / feature report [here].

If you want to cite DSHARP, please use the following bibtex:

@inproceedings{cai-muise-dsharp,
         discipline = {Computer and Information Science},
         author = {Christian Muise and Sheila A Mcilraith and J Christopher Beck and Eric Hsu},
         series = {Canadian Conference on Artificial Intelligence},
         booktitle = {Canadian Conference on Artificial Intelligence},
         title = {{DSHARP}: Fast {d-DNNF} Compilation with {sharpSAT}},
         year = {2012},
         subdiscipline = {Artificial Intelligence},
         type = {Conference Proceedings}
}