Top-Down Knowledge Compilation for Counting Modulo Theories
Vincent Derkinderen, Pedro Zuidberg Dos Martires, Samuel Kolb, Paolo, Morettin

TL;DR
This paper explores top-down knowledge compilation techniques for #SMT problems, extending methods from propositional #SAT to the more complex counting modulo theories setting, using DPLL(T) search traces.
Contribution
It introduces a top-down compilation strategy for #SMT based on DPLL(T) traces, advancing knowledge compilation methods beyond propositional logic.
Findings
Effective top-down compilation approach for #SMT
Extension of propositional #SAT techniques to #SMT
Potential for improved #SMT model counting efficiency
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsBayesian Modeling and Causal Inference · Logic, Reasoning, and Knowledge · Machine Learning and Algorithms
