In Knowledge Compilation (KC) a propositional knowledge base is compiled off-line into some target form, typically into deterministic decomposable negation normal form (d-DNNF) or one of its subcases, which is then used on-line to answer a large number of queries in polytime, such as clausal entailment, model counting, and others. The general idea is to push as much of the computational effort into the off-line compilation phase, which is amortized over all on-line polytime queries. In this paper, we present for the first time a novel and general technique to leverage d-DNNF compilation and querying to SMT level. Intuitively, before d-DNNF compilation, the input SMT formula is combined with a list of pre-computed ad-hoc theory lemmas, so that the queries at SMT level reduce to those at propositional level. This approach has several features: (i) it works for every theory, or theory combination thereof; (ii) it works for all forms of d-DNNF; (iii) it is easy to implement on top of any d-DNNF compiler and any theory-lemma enumerator, which are used as black boxes; (iv) most importantly, these compiled SMT d-DNNFs can be queried in polytime by means of a standard propositional d-DNNF reasoner. As proof of concept, we have implemented a tool on top of state-of-the-art d-DNNF packages and of the MathSAT SMT solver. Some preliminary empirical evaluation supports the effectiveness of the approach.

翻译：在知识编译（KC）中，命题知识库被离线编译为目标形式（通常为确定性可分解否定范式（d-DNNF）或其子类），随后在线用于在多项式时间内回答大量查询（如子句蕴含、模型计数等）。其核心思想是将大部分计算负担转移至离线编译阶段，该成本通过所有在线多项式时间查询得到分摊。本文首次提出一种新颖的通用技术，将d-DNNF编译与查询扩展至SMT层次。直观而言，在d-DNNF编译前，输入SMT公式需与一组预计算的特设理论引理相结合，从而使SMT层面的查询转化为命题层面的查询。该方法具有以下特点：(i) 适用于任意理论或其组合；(ii) 兼容所有形式的d-DNNF；(iii) 易于基于任何d-DNNF编译器和任何理论引理枚举器（作为黑盒组件）实现；(iv) 最重要的是，这些编译后的SMT d-DNNF可通过标准命题d-DNNF推理器在多项式时间内完成查询。作为概念验证，我们在最先进的d-DNNF工具包及MathSAT SMT求解器上实现了相应工具。初步实验评估结果支持了该方法的有效性。