Efficient and Effective Extensions of SMT-Enumeration Techniques for Weighted Model Integration, Optimization, and Knowledge Compilation

Satisfiability Modulo Theories (SMT) enumeration is the problem of enumerating the theory-satisfiable truth assignments propositionally satisfying a given SMT formula. It underlies several tasks in formal verification, automated reasoning, and probabilistic inference. However, the number of such assignments may grow exponentially, limiting the applicability of SMT enumeration to large and complex problems. This dissertation studies how suitable encodings and application-specific strategies can make SMT enumeration effective in practice and enable its use in novel problems. A central focus is the enumeration of few, short partial truth assignments, which compactly represent large sets of total assignments and reduce both enumeration costs and application-specific computation. We make the following contributions. First, we show that standard CNF encodings may inhibit short partial-assignment generation and propose a novel encoding that drastically reduces both the number of assignments and the enumeration time. We then develop a structure-aware encoding and enumeration strategy for Weighted Model Integration, which significantly reduces the number of required integrals and improves upon state-of-the-art methods. We also adapt partial-assignment enumeration to Optimization Modulo Theories, introducing optimization-specific reduction techniques that speed up the solving process. A related decomposition strategy is applied to constrained Maximum A Posteriori inference, enabling the optimization of highly nonlinear density functions through the combination of SMT enumeration and external numerical optimizers. The dissertation then addresses the computation of a complete set of theory lemmas for a given SMT formula. We devise several techniques based on parallel cube-and-conquer and projected enumeration, improving scalability while preserving completeness. These lemmas are then used to define a framework for \dDNNFs{} Modulo Theories, which supports polytime SMT transformations and queries. Extensive experiments support the practical effectiveness and real-world applicability of our contributions.