All-Solution Satisfiability (AllSAT) and its extension, All-Solution Satisfiability Modulo Theories (AllSMT), have become more relevant in recent years, mainly in formal verification and artificial intelligence applications. The goal of these problems is the enumeration of all satisfying assignments of a formula (for SAT and SMT problems, respectively), making them useful for test generation, model checking, and probabilistic inference. Nevertheless, traditional AllSAT algorithms face significant computational challenges due to the exponential growth of the search space and inefficiencies caused by blocking clauses, which cause memory blowups and degrade unit propagation performances in the long term. This paper presents two novel solvers: tabularAllSAT, a projected AllSAT solver, and tabularAllSMT, a projected AllSMT solver. Both solvers combine Conflict-Driven Clause Learning (CDCL) with chronological backtracking to improve efficiency while ensuring disjoint enumeration. To retrieve compact partial assignments we propose a novel aggressive implicant shrinking algorithm, compatible with chronological backtracking, to minimize the number of partial assignments, reducing overall search complexity. Furthermore, we extend the solver framework to handle projected enumeration and SMT formulas effectively and efficiently, adapting the baseline framework to integrate theory reasoning and the distinction between important and non-important variables. An extensive experimental evaluation demonstrates the superiority of our approach compared to state-of-the-art solvers, particularly in scenarios requiring projection and SMT-based reasoning.

翻译：全解可满足性问题（AllSAT）及其扩展——全解可满足性模理论问题（AllSMT），近年来在形式化验证与人工智能应用领域日益重要。这些问题的目标在于枚举公式的所有可满足赋值（分别对应SAT与SMT问题），使其在测试生成、模型检验及概率推理中具有实用价值。然而，传统AllSAT算法因搜索空间的指数级增长及阻塞子句导致的低效性而面临显著计算挑战：阻塞子句长期引发内存爆炸并削弱单元传播性能。本文提出两种新型求解器：tabularAllSAT（投影AllSAT求解器）与tabularAllSMT（投影AllSMT求解器）。两种求解器均将冲突驱动子句学习与时序回溯相结合，在确保不相交枚举的同时提升效率。为获取紧凑部分赋值，我们提出一种与时序回溯兼容的新型激进蕴涵项收缩算法，以最小化部分赋值数量，从而降低整体搜索复杂度。此外，我们将求解器框架扩展至高效处理投影枚举与SMT公式，通过适配基础框架以集成理论推理及重要变量与非重要变量的区分。大量实验评估表明，相较于前沿求解器，我们的方法在需要投影与基于SMT推理的场景中具有显著优势。