Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses

TL;DR

This paper introduces two new solvers for AllSAT and AllSMT problems that improve efficiency and scalability by avoiding blocking clauses and using a novel shrinking algorithm, with extensive experimental validation.

Contribution

The paper presents the first projected AllSAT and AllSMT solvers combining CDCL, chronological backtracking, and a novel implicant shrinking algorithm for disjoint enumeration.

Findings

Outperforms state-of-the-art solvers in projected enumeration scenarios.

Reduces memory usage and search complexity through disjoint enumeration.

Effectively integrates theory reasoning for SMT formulas.

Abstract

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.