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.
Indian Institute of Technology Bombay（印度理工学院班加罗尔分校）；University of Toronto（多伦多大学）；Vector Institute（向量研究所）；Georgia Institute of Technology（佐治亚理工学院）；National University of Singapore（新加坡国立大学）
On the Complexity of SHAP-Score-Based Explanations: Tractability via Knowledge Compilation and Non-Approximability Results
Universidad Católica de Chile（智利天主教大学）；IMFD Chile（智利数学与计算工程研究所）；National Center for Artificial Intelligence, CENIA Chile（智利国家人工智能中心（CENIA））；SKEMA Business School（SKEMA商学院）；Univ. Lille（里尔大学）；Inria（法国国家信息与自动化研究所）；CNRS（法国国家科学研究中心）；Centrale Lille（里尔中央理工学院）
Chennai Mathematical Institute, India IAI, TCG CREST, Kolkata, India（钦奈数学研究所，印度 IAI，TCG CREST，科利尔，印度）；Georgia Institute of Technology, USA University of Toronto, Canada（佐治亚理工学院，美国 蒙特利尔大学，加拿大）
