Efficient and Effective Model Enumeration in SAT and SMT: Investigating Novel Procedures and Applications

Propositional satisfiability (SAT) has long been a cornerstone of computer science, especially in areas like hardware verification and AI. Whereas solving SAT problems has received significant attention, the task of enumerating all satisfying solutions—known as the All-Solution Satisfiability Problem (AllSAT)—remains comparatively underexplored. This thesis addresses the gap in research on AllSAT and its extension to All-Satisfiability Modulo Theories (AllSMT), where both Boolean and first-order logic atoms come into play. We started by introducing a novel algorithm for enumerating disjoint partial models without introducing blocking clauses, by integrating Conflict-Driven Clause Learning, Chronological Backtracking, and implicant shrinking techniques. We further extend this algorithm to handle projected enumeration and AllSMT, incorporating theory reasoning to address the complexities of richer logical frameworks. Dealing with the enumeration of non-Conjunctive Normal Form (non-CNF) formulas poses significant challenges. Traditional transformations such as Tseitin and Plaisted-Greenbaum hinder the production of small partial satisfying assignments, affecting the effectiveness of enumeration. In this thesis, we discuss a novel approach that combines Plaisted-Greenbaum transformation with Negative Normal Form (NNF) preprocessing, dramatically reducing the overall size of partial assignments and thus improving both efficiency and effectiveness of enumeration. Beyond the novel procedures mentioned above, we demonstrate the practical applications of AllSAT and AllSMT in several novel domains. These include (i) Weighted Model Integration (WMI), where AllSMT is used to efficiently reduce the number of integrals required by WMI algorithms based on predicate abstraction; (ii) knowledge compilation (KC), where theory lemmas generated from AllSMT prune inconsistent paths to create canonical decision diagrams; and (iii) quantum computing, where SMT and OMT are used to encode prime factorization problems of biprime numbers into D-Wave quantum annealers.