Click here to flash read.
Propositional model counting (#SAT) can be solved efficiently when the input
formula is in deterministic decomposable negation normal form (d-DNNF).
Translating an arbitrary formula into a representation that allows inference
tasks, such as counting, to be performed efficiently, is called knowledge
compilation. Top-down knowledge compilation is a state-of-the-art technique for
solving #SAT problems that leverages the traces of exhaustive DPLL search to
obtain d-DNNF representations. While knowledge compilation is well studied for
propositional approaches, knowledge compilation for the (quantifier free)
counting modulo theory setting (#SMT) has been studied to a much lesser degree.
In this paper, we discuss compilation strategies for #SMT. We specifically
advocate for a top-down compiler based on the traces of exhaustive DPLL(T)
search.
No creative common's license