Research map / Architectures and efficiency / RNNs and normalization
Disjoint Partial Enumeration without Blocking Clauses
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes a disjoint AllSAT procedure that enumerates disjoint partial models without blocking clauses by combining CDCL, chronological backtracking, and a chronological implicant shrinking algorithm based on 2-watched literals.
Problem
Disjoint AllSAT (enumerating non-overlapping propositional models) is inefficient with blocking clauses, which consume memory and slow unit propagation, while non-blocking solvers only produce total assignments.
Approach
Integrates CDCL with chronological backtracking and a new chronological implicant shrinking procedure (using 2-watched literal lists) so partial models are obtained a posteriori from total trails with no blocking clauses; backtrack reason clauses are virtual (tagged BACKTRUE) rather than stored.
Key results
- The proposed solver solves 1939 of 1960 instances, versus 1935 for BDD, 1915 for NBC, 1715 for MathSAT5, 1440 for BC and 1217 for BC_Partial.
- On rnd3sat, BDD solves 409 instances versus 410 for the proposed solver, which is the only benchmark where it is not best-or-tied.
- The faster conservative literal check outperforms the full watch-updating shrinking variant in CPU time, while the latter yields more compact partial assignments.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use Chrono-CDCL instead of BDD | disjoint partial AllSAT solving · binary clauses | instances solved: 28 -> 30 | Helped |
| Use Chrono-CDCL instead of BDD | disjoint partial AllSAT solving · rnd3sat | instances solved: 409 -> 410 | No clear effect |
| Use Chrono-CDCL instead of BDD or NBC | disjoint partial AllSAT solving · CSB | instances solved: 1000 -> 1000 | No clear effect |
| Use Chrono-CDCL instead of BDD or NBC | disjoint partial AllSAT solving · BMS | instances solved: 498 -> 499 | Helped |
| Use Chrono-CDCL instead of BDD | disjoint partial AllSAT solving · all benchmarks | instances solved: 1935 -> 1939 | Helped |
| Use dynamic watch-list updates instead of conservative literal checking | Chrono-CDCL implicant shrinking · crafted and SATLIB benchmarks | number of partial assignments | Helped |
| Use dynamic watch-list updates instead of conservative literal checking | Chrono-CDCL implicant shrinking · formulas with many satisfying models | CPU time | Hurt |
Surprising findings
- The first UIP stopping criterion can break mutual exclusivity of returned assignments, so the last UIP is required.
- Dynamically updating watch lists yields more compact partial models but is slower overall as the model count grows.
Limitations
- Conservative literal check may miss shrinking opportunities compared to full watch updates.
- Only disjoint (not projected) enumeration is handled.
- Does not use decision heuristics specifically designed for chronological backtracking.
Experimental setup
Datasets: Binary clauses (crafted) Rnd3sat (random 3-SAT) CBS (SATLIB) BMS (SATLIB)
Benchmarks: Binary clauses Rnd3sat CBS BMS
Metrics: number of instances solved within 1200s timeout CPU time number of disjoint partial models
Baselines: BC BC_Partial NBC BDD MathSAT5
Builds on: chronological backtracking calculus for model counting 2-watched literal scheme VSADS MiniSAT
Closest papers by meaning
- Symmetric Component Caching for Model Counting on Combinatorial Instances (AAAI 2021 · similarity 0.85)
- Premise Set Caching for Enumerating Minimal Correction Subsets (AAAI 2018 · similarity 0.85)
- Component Caching in Hybrid Domains with Piecewise Polynomial Densities (AAAI 2016 · similarity 0.85)
- Submodel Enumeration for CTL Is Hard (AAAI 2024 · similarity 0.83)
- Hardness of Random Reordered Encodings of Parity for Resolution and CDCL (AAAI 2024 · similarity 0.82)
- Boule or Baguette? A Study on Task Topology, Length Generalization, and the Benefit of Reasoning Trace (NeurIPS 2026 · similarity 0.82)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.