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.

翻译：命题模型计数（#SAT）在输入公式为确定性可分解否定范式（d-DNNF）时，可被高效求解。将任意公式转化为能够高效执行计数等推理任务的表示形式，称为知识编译。自顶向下知识编译是解决#SAT问题的最新技术之一，它利用穷举DPLL搜索的踪迹来获取d-DNNF表示。尽管命题逻辑中的知识编译已得到充分研究，但针对（无量词）计数模理论设置（#SMT）的知识编译研究仍相当有限。本文探讨了#SMT的编译策略，特别倡导基于穷举DPLL(T)搜索踪迹的自顶向下编译器。