pith. sign in

arxiv: 2410.18707 · v2 · submitted 2024-10-22 · 💻 cs.LO

Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses

Giuseppe Spallitta , Roberto Sebastiani , Armin Biere This is my paper

Pith reviewed 2026-05-23 19:20 UTC · model grok-4.3

classification 💻 cs.LO
keywords AllSATAllSMTprojected enumerationchronological backtrackingblocking clausesimplicant shrinkingCDCLSMT solvers
0
0 comments X

The pith

Disjoint projected AllSAT and AllSMT enumeration works without blocking clauses when CDCL is paired with chronological backtracking.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces solvers called tabularAllSAT and tabularAllSMT that enumerate all satisfying assignments for SAT and SMT formulas while projecting onto a subset of important variables. Traditional approaches rely on blocking clauses to keep solutions disjoint, but these clauses lead to memory growth and slower propagation as the enumeration proceeds. The new method instead uses chronological backtracking together with conflict-driven clause learning to maintain disjointness by construction. It adds an aggressive implicant shrinking procedure that produces compact partial assignments and works with the chosen backtracking order. Experiments indicate the approach outperforms existing solvers, especially on projected instances and those that require theory reasoning.

Core claim

tabularAllSAT and tabularAllSMT integrate Conflict-Driven Clause Learning with chronological backtracking to perform projected AllSAT and AllSMT enumeration in a disjoint manner without blocking clauses; a novel aggressive implicant shrinking algorithm minimizes the size of the emitted partial assignments, and the framework is extended to distinguish important variables and to incorporate theory reasoning.

What carries the argument

Chronological backtracking combined with CDCL to enforce disjoint enumeration without blocking clauses, plus aggressive implicant shrinking to obtain compact partial assignments.

If this is right

  • Memory consumption stays bounded because no blocking clauses are added during long enumerations.
  • Unit propagation efficiency does not degrade over the course of the search.
  • Projected enumeration correctly handles the distinction between important and non-important variables.
  • SMT theory reasoning integrates directly into the enumeration loop without extra blocking overhead.
  • Fewer and smaller partial assignments reduce the total number of search steps.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same chronological-backtracking pattern may be worth testing on enumeration tasks outside SAT and SMT, such as in constraint programming.
  • The implicant-shrinking procedure could be ported to other solvers that already use chronological backtracking.
  • Probabilistic inference tools that rely on complete model enumeration might see runtime gains if they adopt the method.

Load-bearing premise

The benchmarks and instances used in the experiments are representative of the target applications and the observed advantages generalize beyond those specific cases.

What would settle it

A new collection of industrial verification or AI benchmarks on which the new solvers consume more memory or run slower than blocking-clause solvers would falsify the claimed superiority.

Figures

Figures reproduced from arXiv: 2410.18707 by Armin Biere, Giuseppe Spallitta, Roberto Sebastiani.

Figure 1
Figure 1. Figure 1: Scatter plot comparing CPU time and # of partial models with the two implicant [PITH_FULL_IMAGE:figures/full_fig_p026_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Scatter plots comparing TabularAllSAT CPU times against other AllSAT solvers. The x and y axes are log-scaled. TabularAllSAT D4+ModelGraph BDD NBC MathSAT5 BC BC Partial rnd3sat (410) 410 410 409 396 229 194 210 CSB (1000) 1000 1000 1000 1000 997 865 636 BMS (500) 500 500 498 498 473 368 353 Total (1910) 1910 1910 1907 1894 1699 1427 1199 [PITH_FULL_IMAGE:figures/full_fig_p027_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Number of instances solved by each solver within a timeout (1200 seconds) for [PITH_FULL_IMAGE:figures/full_fig_p027_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Scatter plots comparing TabularAllSAT against D4+ModelGraph on All￾SAT problems in [22]. The x and y axes are log-scaled. TabularAllSAT D4+Modelgraph compilation(197) 137 165 competition(246) 99 113 Total(443) 236 289 [PITH_FULL_IMAGE:figures/full_fig_p028_4.png] view at source ↗
Figure 6
Figure 6. Figure 6: Scatter plot comparing CPU time and number of partial assign [PITH_FULL_IMAGE:figures/full_fig_p030_6.png] view at source ↗
Figure 7
Figure 7. 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. TabularAllSAT D4+ModelGraph Dualiza MathSAT5 iscas (100) 100 100 76 78 b25 r0 d6 (250) 250 250 250 174 Total (350) 350 350 326 252 [PITH_FULL_IMAGE:figures/full_fig_p031_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Table reporting the number of instances solved by each solver within the timeout [PITH_FULL_IMAGE:figures/full_fig_p031_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Scatter plot comparing CPU time and number of partial assignments of [PITH_FULL_IMAGE:figures/full_fig_p032_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Scatter plot comparing CPU time for total enumeration (a), CPU time for [PITH_FULL_IMAGE:figures/full_fig_p034_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Table reporting the number of instances solved by each solver within the [PITH_FULL_IMAGE:figures/full_fig_p034_11.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper introduces tabularAllSAT and tabularAllSMT, two solvers for projected AllSAT and AllSMT that achieve disjoint enumeration without blocking clauses. They combine CDCL with chronological backtracking and introduce an aggressive implicant shrinking procedure to produce compact partial assignments. The framework is extended to distinguish important/non-important variables and to integrate theory reasoning for SMT; an experimental section claims superiority over existing solvers on projection-heavy and SMT instances.

Significance. If the reported performance gains hold, the approach would be a practical advance for AllSAT/AllSMT applications in verification and probabilistic inference by eliminating the memory and propagation overhead of blocking clauses while preserving disjointness. The combination of chronological backtracking with shrinking is a concrete algorithmic contribution that could be adopted more broadly.

major comments (2)
  1. [§5] §5 (experimental tables): the superiority claims rest on benchmark runs, yet the text does not report variance across random seeds, statistical significance tests, or the precise distribution of projection-variable cardinalities; without these, it is impossible to judge whether the observed speed-ups are robust or instance-specific.
  2. [§3.2] §3.2 (implicant shrinking): the description of the shrinking procedure is compatible with chronological backtracking, but the manuscript does not supply a short argument or invariant showing that the produced implicants remain disjoint across the entire search tree; this invariant is load-bearing for the central “disjoint without blocking clauses” claim.
minor comments (2)
  1. [§4] Notation for “important” versus “non-important” variables is introduced in §4 but used inconsistently in the pseudocode of Algorithm 2; a single clarifying sentence or footnote would suffice.
  2. [§5] Several figure captions in §5 omit the timeout value and memory limit used for the competing solvers; these parameters should be stated explicitly.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback and the recommendation for major revision. Below we respond point-by-point to the major comments, indicating the revisions we will make to address the concerns.

read point-by-point responses

  1. Referee: [§5] §5 (experimental tables): the superiority claims rest on benchmark runs, yet the text does not report variance across random seeds, statistical significance tests, or the precise distribution of projection-variable cardinalities; without these, it is impossible to judge whether the observed speed-ups are robust or instance-specific.

    Authors: We agree that additional statistical details would strengthen the presentation. The core enumeration procedures are deterministic; any variability arises only from minor heuristic choices in variable ordering. In the revised §5 we will (i) report the distribution of projection-variable cardinalities over the benchmark sets and (ii) add a short paragraph noting that re-runs with varied random seeds produced negligible performance differences, together with standard deviations for any averaged timings. These additions can be made without new experimental campaigns. revision: yes

  2. Referee: [§3.2] §3.2 (implicant shrinking): the description of the shrinking procedure is compatible with chronological backtracking, but the manuscript does not supply a short argument or invariant showing that the produced implicants remain disjoint across the entire search tree; this invariant is load-bearing for the central “disjoint without blocking clauses” claim.

    Authors: We thank the referee for highlighting this omission. Chronological backtracking partitions the search space into disjoint subtrees at each decision point; the shrinking routine only drops literals that are implied by the current prefix and the learned clauses, preserving the coverage of each subtree. We will insert a concise invariant argument (one paragraph plus a short proof sketch) immediately after the description of the shrinking procedure in §3.2. This will be included in the revised manuscript. revision: yes

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper presents new algorithmic solvers (tabularAllSAT, tabularAllSMT) that combine CDCL with chronological backtracking and introduce an aggressive implicant shrinking procedure for projected enumeration. These techniques are described via pseudocode and motivated by concrete implementation details rather than any self-referential definitions or fitted inputs. Central claims of superiority rest on external benchmark comparisons, not on equations or uniqueness theorems that reduce to the authors' prior work by construction. No self-citation is load-bearing for the core results, and the derivation chain consists of standard algorithmic extensions that remain independently verifiable through the supplied implementation and experiments.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The approach rests on standard assumptions from CDCL SAT solving and the feasibility of combining chronological backtracking with theory reasoning; no free parameters or invented entities are introduced in the abstract.

axioms (2)
  • domain assumption CDCL can be combined with chronological backtracking to produce disjoint enumerations without blocking clauses
    Core design choice stated in the abstract for both solvers.
  • domain assumption Aggressive implicant shrinking is compatible with chronological backtracking and reduces search complexity
    Novel component claimed to minimize partial assignments.

pith-pipeline@v0.9.0 · 5779 in / 1230 out tokens · 28414 ms · 2026-05-23T19:20:01.089408+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

46 extracted references · 46 canonical work pages

  1. [1]

    Khurshid, D

    S. Khurshid, D. Marinov, I. Shlyakhter, D. Jackson, A case for efficient solution enumeration, in: Theory and Applications of Satisfiability Test- ing: 6th International Conference, SAT 2003, Santa Margherita Ligure, Italy, May 5-8, 2003, Selected Revised Papers 6, Springer, 2004, pp. 272–286

    work page 2003

  2. [2]

    H. Jin, H. Han, F. Somenzi, Efficient conflict analysis for finding all sat- isfying assignments of a Boolean circuit, in: Tools and Algorithms for 35 the Construction and Analysis of Systems: 11th International Confer- ence, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8...

    work page 2005

  3. [3]

    I. O. Dlala, S. Jabbour, L. Sais, B. B. Yaghlane, A comparative study of SAT-based itemsets mining, in: Research and Development in Intel- ligent Systems XXXIII: Incorporating Applications and Innovations in Intelligent Systems XXIV 33, Springer, 2016, pp. 37–52

    work page 2016

  4. [4]

    Spallitta, G

    G. Spallitta, G. Masina, P. Morettin, A. Passerini, R. Sebastiani, SMT- based weighted model integration with structure awareness, in: Uncer- tainty in Artificial Intelligence, PMLR, 2022, pp. 1876–1885

    work page 2022

  5. [5]

    Spallitta, G

    G. Spallitta, G. Masina, P. Morettin, A. Passerini, R. Sebastiani, En- hancing SMT-based Weighted Model Integration by structure awareness, Artificial Intelligence 328 (2024) 104067

    work page 2024

  6. [6]

    Chistikov, R

    D. Chistikov, R. Dimitrova, R. Majumdar, Approximate counting in SMT and value estimation for probabilistic programs, in: Tools and Algorithms for the Construction and Analysis of Systems: 21st Inter- national Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 201...

    work page 2015

  7. [7]

    Michelutti, G

    M. Michelutti, G. Masina, G. Spallitta, R. Sebastiani, Canonical Deci- sion Diagrams Modulo Theories, IOS Press - ECAI 2024, 2024

    work page 2024

  8. [8]

    S. K. Lahiri, R. Nieuwenhuis, A. Oliveras, SMT techniques for fast pred- icate abstraction, in: Computer Aided Verification: 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006. Pro- ceedings 18, Springer, 2006, pp. 424–437

    work page 2006

  9. [9]

    Gupta, Z

    A. Gupta, Z. Yang, P. Ashar, A. Gupta, SAT-based image computation with application in reachability analysis, in: International Conference on Formal Methods in Computer-Aided Design, Springer, 2000, pp. 391– 408

    work page 2000

  10. [10]

    Grumberg, A

    O. Grumberg, A. Schuster, A. Yadgar, Memory efficient all-solutions SAT solver and its application for reachability analysis, in: Formal 36 Methods in Computer-Aided Design: 5th International Conference, FM- CAD 2004, Austin, Texas, USA, November 15-17, 2004. Proceedings 5, Springer, 2004, pp. 275–289

    work page 2004

  11. [11]

    Brauer, A

    J. Brauer, A. King, J. Kriener, Existential quantification as incremen- tal SAT, in: Computer Aided Verification: 23rd International Confer- ence, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings 23, Springer, 2011, pp. 191–207

    work page 2011

  12. [12]

    O. Shtrichman, Pruning techniques for the SAT-based bounded model checking problem, in: Advanced Research Working Conference on Cor- rect Hardware Design and Verification Methods, Springer, 2001, pp. 58–70

    work page 2001

  13. [13]

    K. L. McMillan, Applying SAT methods in unbounded symbolic model checking, in: Computer Aided Verification: 14th International Confer- ence, CAV 2002 Copenhagen, Denmark, July 27–31, 2002 Proceedings 14, Springer, 2002, pp. 250–264

    work page 2002

  14. [14]

    Y. Yu, P. Subramanyan, N. Tsiskaridze, S. Malik, All-SAT using min- imal blocking clauses, in: 2014 27th International Conference on VLSI Design and 2014 13th International Conference on Embedded Systems, IEEE, 2014, pp. 86–91

    work page 2014

  15. [15]

    B. Li, M. S. Hsiao, S. Sheng, A novel SAT all-solutions solver for efficient preimage computation, in: Proceedings Design, Automation and Test in Europe Conference and Exhibition, Vol. 1, IEEE, 2004, pp. 272–277

    work page 2004

  16. [16]

    Nadel, V

    A. Nadel, V. Ryvchin, Chronological backtracking, in: Theory and Ap- plications of Satisfiability Testing–SAT 2018: 21st International Confer- ence, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9–12, 2018, Proceedings 21, Springer, 2018, pp. 111–121

    work page 2018

  17. [17]

    M¨ ohle, A

    S. M¨ ohle, A. Biere, Combining conflict-driven clause learning and chronological backtracking for propositional model counting., in: GCAI, 2019, pp. 113–126

    work page 2019

  18. [18]

    Sebastiani, Are you satisfied by this partial assignment?, arXiv preprint arXiv:2003.04225 (2020)

    R. Sebastiani, Are you satisfied by this partial assignment?, arXiv preprint arXiv:2003.04225 (2020). 37

    work page arXiv 2003

  19. [19]

    Fried, A

    D. Fried, A. Nadel, R. Sebastiani, Y. Shalmon, Entailing generaliza- tion boosts enumeration, in: 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024), Schloss Dagstuhl– Leibniz-Zentrum f¨ ur Informatik, 2024

    work page 2024

  20. [20]

    M¨ ohle, R

    S. M¨ ohle, R. Sebastiani, A. Biere, Four flavors of entailment, in: Interna- tional Conference on Theory and Applications of Satisfiability Testing, Springer, 2020, pp. 62–71

    work page 2020

  21. [21]

    M¨ ohle, R

    S. M¨ ohle, R. Sebastiani, A. Biere, On Enumerating Short Projected Models, Discrete Applied Mathematics 361 (2025) 412–439. doi:10. 1016/j.dam.2024.10.021

    work page 2025

  22. [22]

    Lagniez, E

    J.-M. Lagniez, E. Lonca, Leveraging Decision-DNNF Compilation for Enumerating Disjoint Partial Models, in: 21st International Conference on Principles of Knowledge Representation and Reasoning (KR 2024), 2024

    work page 2024

  23. [23]

    M¨ ohle, An Abstract CNF-to-d-DNNF compiler based on chronolog- ical CDCL, in: International Symposium on Frontiers of Combining Systems, Springer, 2023, pp

    S. M¨ ohle, An Abstract CNF-to-d-DNNF compiler based on chronolog- ical CDCL, in: International Symposium on Frontiers of Combining Systems, Springer, 2023, pp. 195–213

    work page 2023

  24. [24]

    Cimatti, A

    A. Cimatti, A. Griggio, B. J. Schaafsma, R. Sebastiani, The MathSAT5 SMT solver, in: Tools and Algorithms for the Construction and Analysis of Systems: 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings 19, Springer, 2013, pp. 93–107

    work page 2013

  25. [25]

    Spallitta, R

    G. Spallitta, R. Sebastiani, A. Biere, Disjoint partial enumeration with- out blocking clauses, in: Proceedings of the AAAI Conference on Arti- ficial Intelligence, Vol. 38, 2024, pp. 8126–8135

    work page 2024

  26. [26]

    G. S. Tseitin, On the Complexity of Derivation in Propositional Calcu- lus, in: Automation of Reasoning: 2: Classical Papers on Computational Logic 1967–1970, Symbolic Computation, Springer, 1983, pp. 466–483

    work page 1967

  27. [27]

    D. A. Plaisted, S. Greenbaum, A Structure-preserving Clause Form Translation, Journal of Symbolic Computation 2 (3) (1986) 293–304. doi:10.1016/S0747-7171(86)80028-1. 38

    work page doi:10.1016/s0747-7171(86)80028-1 1986

  28. [28]

    Masina, G

    G. Masina, G. Spallitta, R. Sebastiani, On CNF conversion for disjoint SAT enumeration, in: 26th International Conference on Theory and Ap- plications of Satisfiability Testing (SAT 2023), Schloss-Dagstuhl-Leibniz Zentrum f¨ ur Informatik, 2023

    work page 2023

  29. [29]

    M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, S. Malik, Chaff: Engineering an efficient SAT solver, in: Proceedings of the 38th annual Design Automation Conference, 2001, pp. 530–535

    work page 2001

  30. [30]

    J. P. Marques-Silva, K. A. Sakallah, GRASP: A search algorithm for propositional satisfiability, IEEE Transactions on Computers 48 (5) (1999) 506–521

    work page 1999

  31. [31]

    Davis, G

    M. Davis, G. Logemann, D. Loveland, A machine program for theorem- proving, Communications of the ACM 5 (7) (1962) 394–397

    work page 1962

  32. [32]

    R. J. Bayardo Jr, J. D. Pehoushek, Counting models using connected components, in: AAAI/IAAI, 2000, pp. 157–162

    work page 2000

  33. [33]

    Morgado, J

    A. Morgado, J. Marques-Silva, Good learning and implicit model enu- meration, in: 17th IEEE International Conference on Tools with Artifi- cial Intelligence (ICTAI’05), IEEE, 2005, pp. 6–pp

    work page 2005

  34. [34]

    M¨ ohle, A

    S. M¨ ohle, A. Biere, Backing backtracking, in: Theory and Applications of Satisfiability Testing–SAT 2019: 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9–12, 2019, Proceedings 22, Springer, 2019, pp. 250–266

    work page 2019

  35. [35]

    Huang, A

    J. Huang, A. Darwiche, Using DPLL for efficient OBDD construction, in: Theory and Applications of Satisfiability Testing: 7th International Conference, SAT 2004, Vancouver, BC, Canada, May 10-13, 2004, Re- vised Selected Papers 7, Springer, 2005, pp. 157–172

    work page 2004

  36. [36]

    T. Toda, T. Soh, Implementing efficient all solutions SAT solvers, Jour- nal of Experimental Algorithmics (JEA) 21 (2016) 1–44

    work page 2016

  37. [37]

    Spallitta, A

    G. Spallitta, A. Biere, R. Sebastiani, Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses: TabularAllSAT source code (Nov. 2024). doi:10.5281/zenodo.14197776. URL https://doi.org/10.5281/zenodo.14197776 39

    work page doi:10.5281/zenodo.14197776 2024

  38. [38]

    R. J. Bayardo Jr, R. Schrag, Using CSP look-back techniques to solve real-world SAT instances, in: Aaai/iaai, Citeseer, 1997, pp. 203–208

    work page 1997

  39. [39]

    Singer, I

    J. Singer, I. P. Gent, A. Smaill, Backbone fragility and the local search cost peak, Journal of Artificial Intelligence Research 12 (2000) 235–270

    work page 2000

  40. [40]

    Sharma, S

    S. Sharma, S. Roy, M. Soos, K. S. Meel, GANAK: A scalable prob- abilistic exact model counter, in: Proceedings of International Joint Conference on Artificial Intelligence (IJCAI), 2019

    work page 2019

  41. [41]

    Zhang, G

    Y. Zhang, G. Pu, J. Sun, Accelerating All-SAT computation with short blocking clauses, in: Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering, 2020, pp. 6–17

    work page 2020

  42. [42]

    Liang, F

    J. Liang, F. Ma, J. Zhou, M. Yin, AllSATCC: Boosting AllSAT Solving with Efficient Component Analysis, in: IJCAI, 2022, pp. 1866–1872

    work page 2022

  43. [43]

    Fried, A

    D. Fried, A. Nadel, Y. Shalmon, AllSAT for combinational circuits, in: 26th International Conference on Theory and Applications of Satisfia- bility Testing (SAT 2023), Schloss Dagstuhl-Leibniz-Zentrum f¨ ur Infor- matik, 2023

    work page 2023

  44. [44]

    M¨ ohle, A

    S. M¨ ohle, A. Biere, Dualizing projected model counting, in: 2018 IEEE 30th International Conference on Tools with Artificial Intelligence (IC- TAI), IEEE, 2018, pp. 702–709

    work page 2018

  45. [45]

    Spallitta, A

    G. Spallitta, A. Biere, R. Sebastiani, Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses: TabularAllSMT (Nov. 2024). doi:10.5281/zenodo.14198207. URL https://doi.org/10.5281/zenodo.14198207

    work page doi:10.5281/zenodo.14198207 2024

  46. [46]

    Masina, G

    G. Masina, G. Spallitta, R. Sebastiani, On CNF Conversion for SAT and SMT enumeration, arXiv preprint arXiv:2303.14971 (2023). 40

    work page arXiv 2023