Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses

Giuseppe Spallitta, Roberto Sebastiani, Armin Biere

TL;DR

Two novel solvers are presented: tabularAllSAT, a projected AllSAT solver, and tabularAllSMT, a projected AllSMT solver that combines Conflict-Driven Clause Learning with chronological backtracking to improve efficiency while ensuring disjoint enumeration.

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.

Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses

TL;DR

Two novel solvers are presented: tabularAllSAT, a projected AllSAT solver, and tabularAllSMT, a projected AllSMT solver that combines Conflict-Driven Clause Learning with chronological backtracking to improve efficiency while ensuring disjoint enumeration.

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.

Paper Structure

This paper contains 32 sections, 12 equations, 7 figures, 8 algorithms.

Table of Contents

  1. Introduction
  2. Computational Challenges in Enumeration
  3. Related work
  4. Our Contribution
  5. Disclaimer
  6. Structure of the paper
  7. Background
  8. Notation
  9. AllSAT, AllSMT and Projection
  10. The 2-Watched Literal Scheme
  11. CDCL and Non-chronological Backtracking
  12. Chronological Backtracking
  13. Benefits and Drawbacks of CDCL and CB for Enumeration
  14. Enumerating Disjoint Partial Models without Blocking Clauses
  15. Disjoint AllSAT by Integrating CDCL and CB
  16. ...and 17 more sections

Figures (7)

  • Figure 1: Scatter plot comparing CPU time and # of partial models with the two implicant shrinking algorithms. The $x$ and $y$ axes are log-scaled.
  • Figure 2: Scatter plots comparing TabularAllSAT CPU times against other AllSAT solvers. The $x$ and $y$ axes are log-scaled.
  • Figure 4: Scatter plots comparing TabularAllSAT against D4+ModelGraph on AllSAT problems in lagniez2024leveraging. The $x$ and $y$ axes are log-scaled.
  • Figure 6: Scatter plot comparing CPU time and number of partial assignments generated of TabularAllSAT against the implicant shrinking algorithm of TabularAllSAT$_{AAAI24}$ on projected AllSAT problems. The $x$ and $y$ axes are log-scaled.
  • Figure 7: Scatter plot comparing CPU time of TabularAllSAT against Dualiza, MathSAT5, and D4+ModelGraph on projected AllSAT problems. The $x$ and $y$ axes are log-scaled.
  • ...and 2 more figures

Theorems & Definitions (10)

  • Definition 1
  • Definition 2
  • Definition 3
  • Definition 4
  • Example 1
  • Example 2
  • Example 3
  • Example 4
  • Example 5
  • Example 6