Disjoint Partial Enumeration without Blocking Clauses

Technical Summary: Disjoint Partial Enumeration without Blocking Clauses

Problem Statement
The All-Solution Satisfiability Problem (AllSAT) requires finding all satisfying assignments for a propositional formula. While explicit enumeration of total assignments is often infeasible due to exponential space complexity, using partial models (implicants) allows for compact representations of solution sets. A critical distinction exists between enumeration with repetitions and disjoint enumeration (disjoint AllSAT), where each total assignment must be covered exactly once. Disjoint enumeration is essential for applications such as Weighted Model Integration and #SMT.

Current approaches to disjoint AllSAT generally fall into two categories:

1. Blocking Solvers: These use Conflict-Driven Clause Learning (CDCL) with Non-Chronological Backtracking (NCB). After finding a model, they add "blocking clauses" to prevent the solver from revisiting the same assignment. While effective at pruning the search space, this approach suffers from memory consumption and performance degradation as the number of blocking clauses grows exponentially with the number of models, slowing down unit propagation.
2. Non-Blocking Solvers: These utilize Chronological Backtracking (CB) to avoid blocking clauses. However, traditional CB-based solvers often generate only total assignments and struggle to escape non-satisfiable regions of the search space efficiently without the guidance of learned conflict clauses.

Methodology
The authors propose a novel AllSAT procedure, implemented in a tool called TABULARALLSAT, which integrates three core techniques to achieve disjoint partial enumeration without blocking clauses:

1. CDCL for Search Pruning: The algorithm employs standard CDCL to learn conflict clauses and escape search branches where no satisfying assignments exist. This prevents the solver from getting stuck in unsatisfiable sub-trees, a common weakness of pure CB approaches.
2. Chronological Backtracking (CB) for Termination: Instead of using NCB and adding blocking clauses, the solver uses CB. Upon finding a model, it backtracks to the most recently assigned decision variable and flips its value. This systematic exploration guarantees that no assignment is covered twice without the need for explicit blocking clauses.
3. Chronological Implicant Shrinking: To generate partial models rather than just total ones, the algorithm shrinks total trails post-hoc.
   • It utilizes the 2-Watched Literal Scheme to efficiently check if a literal is necessary for a clause's satisfaction.
   • It introduces a conservative, faster variant of literal checking that avoids updating watch lists during shrinking, trading some minimization depth for significant speed gains.
   • It employs Implicit Solution Reasons: Instead of storing "backtrack reason clauses" in memory (which would defeat the purpose of avoiding blocking clauses), the solver reconstructs them on-the-fly during conflict analysis using a special BACKTRUE tag for flipped literals.

Key Contributions

• Novel Algorithm: The paper presents the first practical implementation of a disjoint AllSAT solver that combines CDCL, Chronological Backtracking, and Implicant Shrinking without relying on blocking clauses.
• Theoretical Foundation: The work builds upon the formal calculus proposed by Möhle and Biere (2019b), adapting it to modern SAT solver data structures and addressing practical implementation gaps (e.g., handling partial trails in solvers that typically detect satisfaction only on total trails).
• Efficient Data Structures: The introduction of implicit backtrack reasons and the conservative literal checking variant allows the solver to maintain high performance and low memory overhead even when enumerating a vast number of models.
• Decision Heuristics: The authors propose a specific variable ordering heuristic (based on VSADS, DLCS, and VSIDS) tailored for chronological backtracking to optimize the number of partial trails retrieved.

Experimental Results
The authors evaluated TABULARALLSAT against state-of-the-art solvers, including blocking solvers (BC, BC PARTIAL), non-blocking solvers (NBC), BDD-based solvers (BDD), and MathSAT5. The benchmarks included crafted binary clause instances, random 3-SAT instances (Rnd3sat), and SATLIB benchmarks (CBS, BMS).

• Performance: TABULARALLSAT solved the highest number of instances across nearly all benchmarks within the 1200-second timeout. It significantly outperformed blocking solvers (BC, MathSAT) and non-blocking solvers (NBC) in terms of the total number of solved instances.
• Comparison with BDD: On the Rnd3sat benchmark (low clause-to-variable ratio), the BDD-based solver outperformed TABULARALLSAT. The authors attribute this to the structural simplicity of these instances, which allows for efficient BDD compilation. However, on more complex benchmarks (BMS, CBS), TABULARALLSAT demonstrated superior performance.
• Shrinking Techniques: Experiments comparing the two implicant shrinking variants showed that while the watch-list-based method produces more compact partial assignments, the "lighter" conservative variant is computationally faster and more effective for overall time efficiency, especially when the number of models is high.

Significance and Claims
The paper claims that the integration of CDCL and Chronological Backtracking effectively mitigates the primary drawbacks of existing disjoint AllSAT approaches: it avoids the memory and propagation bottlenecks caused by blocking clauses while simultaneously avoiding the inefficiency of getting stuck in unsatisfiable search regions. The experimental results demonstrate that this hybrid approach is a viable and often superior alternative for enumerating disjoint partial models, particularly for formulas with a high number of solutions. The authors modestly note that while their approach is highly effective, it may not be the optimal choice for all structural types of formulas (e.g., those easily compiled to BDDs) and suggest future work in decision heuristics and component caching.