Pith. sign in

REVIEW 2 major objections 6 minor 1 cited by

New Algorithms for #2-SAT and #3-SAT

T0 review · 2 major / 6 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper proves that weighted model counting on 2-CNF formulas is solvable in O*(1.1082^m) time and on 3-CNF formulas in O*(1.4423^m) time, improving prior upper bounds for #2-SAT and #3-SAT.

desk verdict Worth refereeing, but the #2-SAT proof has a real gap in Lemma 9; the #3-SAT side is the stronger part. read the letter →

arxiv 2507.14504 v1 pith:X4XRNNPJ submitted 2025-07-19 cs.DS

Junqiang Peng , Zimo Sheng , Mingyu Xiao This is my paper · ORCID
classification cs.DS
keywords weightedmodelcounting#2-SAT#3-SATbranch-and-searchpathdecompositionpathwidthCNFformulaexactalgorithms
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

This paper aims to prove faster worst-case algorithms for counting satisfying assignments of Boolean formulas whose clauses have at most two or three literals, including the weighted version where each literal carries a weight. It claims that weighted #2-SAT can be solved in O*(1.1082^m) time and weighted #3-SAT in O*(1.4423^m) time, where m is the number of clauses. These bounds improve the previous #2-SAT upper bound and supply a valid clause-count algorithm for #3-SAT, whose earlier analysis is shown to be flawed. Model counting is #P-complete and underpins probabilistic inference, reliability estimation, and explainable-AI tasks, so tighter worst-case bounds for restricted clause lengths advance both theory and practice.

What carries the argument

The machinery is a two-stage hybrid of branch-and-search and pathwidth dynamic programming. Path decompositions arrange a graph's vertices into overlapping bags along a line so that each edge appears in some bag, and the pathwidth is the maximum bag size minus one; the algorithms rely on a known bound that expresses pathwidth through the numbers of low-degree vertices. Nine reduction rules simplify formulas without changing the weighted model count, including rules that eliminate duplicate literals, tautologies, subsumed clauses, unit clauses, unused variables, and constant-size components. The central inequality Lemma 9 lower-bounds how much branching on a variable decreases m for 2-CNF formulas, producing branching vectors no worse than (5,11) and (4,11), while Lemma 13 bounds the decrease of the hybrid measure for 3-CNF formulas and yields the four α-dependent branching vectors used to balance the runtime.

What would settle it

Enumerate all reduced 2-CNF and 3-CNF formulas up to a fixed size and record the actual clause-decrease pairs from each branch plus the pathwidth of the remaining primal or dual graph; a single branch worse than the claimed vectors, or a remaining graph whose pathwidth exceeds the claimed (4/27+ε)m or (1/6+ε)m ratio, would refute the corresponding theorem.

Watch

Extended reading notes

Core claim

The central claim is that two algorithms, Alg2CNF and Alg3CNF, solve weighted model counting on 2-CNF and 3-CNF formulas in O*(1.1082^m) and O*(1.4423^m) time respectively. Both algorithms exhaustively apply nine reduction rules, then branch on high-degree variables, and finally, once only low-degree variables remain, build a path decomposition of the primal graph for #2-SAT or the dual graph for #3-SAT and run a pathwidth-based dynamic program. The #2-SAT analysis shows that the remaining primal graph has pathwidth at most (4/27+ε)m, giving phase-three time O*(1.1082^m); the #3-SAT analysis uses the measure μ(F)=m3(F)+α·m2(F) with α=0.6309297 and exploits a degree-at-most-2 dual graph to reach O*(1.4423^m). The paper also documents a flaw in the previous #3-SAT analysis: assigning a value to the chosen variable need not remove any clause, so the old branching vector of (2,2) was unjustified.

Load-bearing premise

The load-bearing assumption is that the known path-decomposition dynamic programs for counting satisfying assignments can be adapted to weighted model counting with the same O*(2^p) running time, and the paper asserts this adaptation without supplying details or a reference.

Editorial extensions

If this is right

  • Unweighted #2-SAT and #3-SAT inherit the same upper bounds, since unweighted counting is the special case of weighted model counting with all literal weights equal.
  • The #2-SAT bound O*(1.1082^m) improves on the previous O*(1.1892^m) algorithm of Zhou et al.
  • The #3-SAT bound O*(1.4423^m) is the first valid worst-case clause-count algorithm of that form for #3-SAT, because the earlier analysis failed to guarantee a clause decrease in every branch.
  • Because the algorithms solve the weighted problem directly, applications such as probabilistic inference and explainable-AI reasoning inherit the improved worst-case guarantee in clause count.
  • The branch-then-path-decompose recipe, with a tunable clause-length measure, may apply to other counting problems parameterized by the number of clauses.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • I would not treat the constants 1.1082 and 1.4423 as tight: the pathwidth bounds use worst-case degree distributions, and refined structural arguments could push them lower without changing the framework.
  • The weighted adaptation of the path-decomposition dynamic programs is worth testing directly: if literal weights force the DP tables to store sums over weighted products rather than plain counts, the O*(2^p) phase-three claim could fail on weighted formulas even though unweighted counting works.
  • A practical implementation could use this algorithm as a fallback for low-degree cores in modern model counters, since the phase-three structures (maximum degree 4 for 2-CNF and 2 for 3-CNF) are exactly the hard-to-branch cores that current counters handle heuristically.
  • The same hybrid measure idea may extend to k-CNF formulas for k>3 with more clause-length parameters, although the paper leaves whether any constant c<2 exists for fixed k as an open question.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 6 minor

Summary. The paper proposes two algorithms for weighted model counting. Alg2CNF solves WMC on 2-CNF formulas in claimed O*(1.1082^m) time, and Alg3CNF solves WMC on 3-CNF formulas in claimed O*(1.4423^m) time, where m is the number of clauses. The algorithms combine nine reduction rules, simple branching on high-degree variables, and phase-three calls to path-decomposition-based dynamic programming. The paper also reuses a pathwidth bound of Fomin et al. to control low-degree residual formulas and includes an appendix explaining a flaw in the earlier #3-SAT analysis of Zhou et al.

Significance. If the claimed bounds are correct, the paper gives a substantial improvement over the previous clause-parameter #2-SAT bound of O*(1.1892^m) and provides the first valid clause-parameter bound for weighted #3-SAT at O*(1.4423^m). The overall framework, combining a small set of reduction rules with a pathwidth phase, is attractive and could be useful beyond the two problems treated here. The reduction-rule correctness proofs and the #3-SAT measure analysis are largely clear. However, the proof of the central #2-SAT branching lemma contains a concrete false claim, and the weighted version of the path-decomposition algorithms is asserted without proof; both points must be repaired before the main theorems are fully supported.

major comments (2)
  1. [Section 4.1, Lemma 9, Eq. (4)] The proof that q>=3 + q2 >= 2 for every reduced formula is incomplete: the argument applies R-Rule 8 to F1 = S0 union S1 union S2 and F2 = F \ F1 only when both subformulas are non-empty, but the case F2 = empty is not excluded. This is not merely a formal gap. Consider the reduced 2-CNF formula F = (x v a_i) for 1 <= i <= 5 together with (a_i v a_{i+1}) for 1 <= i <= 5 with indices modulo 5. For this formula d = 5, N2(x) is empty, q2 = q>=3 = 0, F1 = F and F2 is empty; none of R-Rules 8 or 9 applies, and branching on x gives Delta_t = 5 and Delta_f = 10, so Delta_t + Delta_f = 15 < 16, contradicting Lemma 9(2). The problem also appears at the Line-8 branching: the analogous 4-variable construction with a K4 on the neighbors of x gives the branch vector (4,10), whose branching factor is about 1.1115, larger than the phase-three base 2^(4/27) which is about 1.1082. Since Lemma 10 and Lemma 11 derive their branching vectors from Lemma 9(2), the proof of Theorem 4 as written does not establish the claimed O*(1.1082^m) bound. A repair appears possible by restricting Lemma 9 to sufficiently large connected formulas and absorbing the bounded-size exceptions with the brute-force base, but that restriction and the resulting recurrence analysis are not present in the manuscript.
  2. [Section 2.2, Theorems 2 and 3] The paper states that the Samer-Szeider algorithms for #SAT can be adapted to solve the weighted version without increasing the time complexity, but it gives no proof, no construction, and no citation for a weighted version. Both Alg2CNF at Line 11 and Alg3CNF at Line 8 terminate by invoking these algorithms, so the claimed weighted bounds depend on this adaptation. In particular, the weighted dynamic program must maintain products of literal weights over the bags of the path decomposition, and the table size and transition complexity need to be stated precisely to confirm that the O*(2^p) time carries over with p as the pathwidth. Without this information, the weighted claims are not fully supported.
minor comments (6)
  1. [Section 1] In the paragraph beginning 'This paper focuses on #SAT', the phrase 'For comprehensive surveys, For comprehensive surveys' is duplicated.
  2. [Lemma 12 proof] The word 'fomrula' should be 'formula'.
  3. [Lemma 13 proof] The word 'decreses' should be 'decreases'.
  4. [Lemma 9 and Figure 1] In the partition written as 'Sin_3 union Sout_3', the subscript 3 is likely intended to be 2; as written it conflicts with the definition of S2.
  5. [Lemma 12, Eq. (6)] The displayed expression 'm = 2n2 + 3n3 + 4n4 / 2' is ambiguous; the numerator should be parenthesized as (2n2 + 3n3 + 4n4)/2.
  6. [Table 1] The phase-three entry '1.1225 1/alpha = 1.2011' is easy to misread; the text should explicitly state that the phase-three base is 1.1225^(1/alpha) approximately 1.2011 when alpha = 0.6309297.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the runtime bounds are proven against external pathwidth and dynamic-programming results, and the branching analyses are self-contained rather than fitted as predictions.

full rationale

I examined the derivation chain for the two main results. Theorem 4 (the O*(1.1082^m) bound for weighted #2-SAT) is obtained from reduction rules, two branching lemmas, and a phase-three pathwidth argument. Lemma 9 is proved by analyzing, for a branched variable x, how many clauses in the sets S0, S1, and S2 disappear from R(F[x=1]) and R(F[x=0]); the claimed bounds are then converted into branching vectors. Nothing in this chain defines a quantity in terms of the claimed output, and no parameter is fitted to the target result. The bounds are proven inequalities for arbitrary reduced 2-CNF formulas. Theorem 5 (the O*(1.4423^m) bound for weighted #3-SAT) uses the measure mu(F) = m3(F) + alpha*m2(F), with alpha chosen after the analysis to minimize the maximum branching factor. Alpha is a design parameter of the algorithm, not a fitted or data-dependent quantity, and the proof is carried out for the fixed value alpha = 0.6309297. The phase-three bounds rely on Theorem 1 of Fomin et al. and on Theorems 2 and 3 attributed to Samer and Szeider. I checked the self-citation patterns: references [5] and [32] by the present authors are related-work upper bounds and are not load-bearing for the new proofs, and reference [34] is the prior work whose #3-SAT analysis the paper explicitly criticizes in Appendix A. The claim that the Samer-Szeider DP can be adapted to weighted counting with no increase in time is stated without proof, which is a correctness or completeness risk, but it is an external cited result rather than a self-referential premise, so it does not constitute circularity. I also considered the known scrutiny point about Lemma 9(2): the assertion that q>=3 + q2 >= 2 for every reduced formula can fail on constant-size reduced formulas, for example a 5-cycle gadget where q2 = q>=3 = 0 and no split rule applies. That is a potential correctness gap in the proof of the (5,11) and (4,11) branching vectors, not an equivalence between premise and conclusion, so it is outside the scope of a circularity finding. Because the central derivations are self-contained with respect to external hardness results and no prediction is an input renamed as an output, the appropriate finding is no significant circularity.

Assumptions & free parameters 1 free parameters · 3 assumptions · 0 invented entities

The only hand-tuned quantity is alpha; the rest of the analysis rests on cited pathwidth and dynamic-programming results plus the paper's own reduction rules.

free parameters (1)
  • alpha (coefficient of m2 in the #3-SAT measure) = 0.6309297 (log_3 2)
    Hand-chosen to balance the branching factors in phase two against the phase-three pathwidth base; the claimed O*(1.4423^m) bound depends on this choice.
assumptions (3)
  • standard math Theorem 1 pathwidth bound pw(G) <= n3/6 + n4/3 + n>=5 + eps n (Fomin et al.)
    Used in Lemma 12 and Lemma 15 to bound phase-three pathwidth; accepted as background from [17].
  • domain assumption Samer-Szeider path decomposition algorithms for WMC run in O*(2^p) time
    Theorems 2 and 3; the paper states a weighted adaptation exists with minor modifications but does not prove or cite it.
  • domain assumption Positive integer literal weights and standard CNF reductions preserve the weighted count
    Definition 1 and Lemmas 2 to 5; standard but load-bearing for R-Rule 7's weight updates.

how reviews work

0 comments
Cite this review

Pith. "Pith review of New Algorithms for #2-SAT and #3-SAT." pith.science (2026). https://pith.science/paper/X4XRNNPJ

@misc{pith2026250714504,
  author       = {Pith},
  title        = {Pith review of: New Algorithms for #2-SAT and #3-SAT},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/X4XRNNPJ}},
  note         = {Machine review of arXiv:2507.14504}
}
abstract

The #2-SAT and #3-SAT problems involve counting the number of satisfying assignments (also called models) for instances of 2-SAT and 3-SAT, respectively. In 2010, Zhou et al. proposed an $\mathcal{O}^*(1.1892^m)$-time algorithm for #2-SAT and an efficient approach for #3-SAT, where $m$ denotes the number of clauses. In this paper, we show that the weighted versions of #2-SAT and #3-SAT can be solved in $\mathcal{O}^*(1.1082^m)$ and $\mathcal{O}^*(1.4423^m)$ time, respectively. These results directly apply to the unweighted cases and achieve substantial improvements over the previous results. These advancements are enabled by the introduction of novel reduction rules, a refined analysis of branching operations, and the application of path decompositions on the primal and dual graphs of the formula.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. A Hypergraph Container Method for Spread SAT: Approximation and Speedup

    math.CO 2026-04 unverdicted novelty 6.0 of 10

    SAT formulas with (λ,p)_k-structures admit sub-exponential Gap-SAT algorithms whose speedup is controlled by the spread parameter λ, via hypergraph containers.

Reference graph

Works this paper leans on

42 extracted references · 27 canonical work pages · cited by 1 Pith paper

  1. [1]

    Algorithms and complexity results for #sat and bayesian inference

    Fahiem Bacchus, Shannon Dalmao, and Toniann Pitassi. Algorithms and complexity results for #sat and bayesian inference. In 44th Symposium on Foundations of Computer Science (FOCS 2003), 11-14 October 2003, Cambridge, MA, USA, Proceedings, pages 340–351. IEEE Computer Society,

    work page 2003

  2. [2]

    3-coloring in time o(1.3289 n)

    Richard Beigel and David Eppstein. 3-coloring in time o(1.3289 n). J. Algorithms, 54(2):168–204,

    work page

  3. [3]

    Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications

    Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications . IOS Press,

    work page

  4. [4]

    On probabilistic inference by weighted model counting

    Mark Chavira and Adnan Darwiche. On probabilistic inference by weighted model counting. Artif. Intell., 172(6-7):772–799, 2008. doi: 10.1016/J.ARTINT.2007.11.002. URL https://doi.org/10. 1016/j.artint.2007.11.002

    doi:10.1016/j.artint.2007.11.002 2008

  5. [5]

    An improved upper bound for SAT

    Huairui Chu, Mingyu Xiao, and Zhe Zhang. An improved upper bound for SAT. In Thirty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2021, Thirty-Third Conference on Innovative Ap- plications of Artificial Intelligence, IAAI 2021, The Eleventh Symposium on Educational Advances in Artificial Intelligence, EAAI 2021, Virtual Event, February 2-9, 2021,...

    work page doi:10.1609/aaai.v35i5.16487 2021

  6. [6]

    Stephen A. Cook. The complexity of theorem-proving procedures. In Michael A. Harrison, Ranan B. Banerji, and Jeffrey D. Ullman, editors, Proceedings of the 3rd Annual ACM Sympo- sium on Theory of Computing, May 3-5, 1971, Shaker Heights, Ohio, USA, pages 151–158. ACM,

    work page 1971

  7. [7]

    On problems as hard as CNF-SAT

    Marek Cygan, Holger Dell, Daniel Lokshtanov, D ´aniel Marx, Jesper Nederlof, Yoshio Okamoto, Ramamohan Paturi, Saket Saurabh, and Magnus Wahlstr ¨om. On problems as hard as CNF-SAT. ACM Trans. Algorithms, 12(3):41:1–41:24, 2016. doi: 10.1145/2925416. URL https://doi.org/10. 1145/2925416

    doi:10.1145/2925416 2016

  8. [8]

    Counting models for 2sat and 3sat for- mulae

    Vilhelm Dahll ¨of, Peter Jonsson, and Magnus Wahlstr ¨om. Counting models for 2sat and 3sat for- mulae. Theor. Comput. Sci., 332(1-3):265–291, 2005. doi: 10.1016/J.TCS.2004.10.037. URL https://doi.org/10.1016/j.tcs.2004.10.037

    work page doi:10.1016/j.tcs.2004.10.037 2005

Show all 42 references
  1. [9]

    Counting the number of solutions for instances of satisfiability

    Olivier Dubois. Counting the number of solutions for instances of satisfiability. Theor. Com- put. Sci., 81(1):49–64, 1991. doi: 10.1016/0304-3975(91)90315-S. URL https://doi.org/10.1016/ 0304-3975(91)90315-S

    1991 doi

  2. [10]

    Dudek, Vu H

    Jeffrey M. Dudek, Vu H. N. Phan, and Moshe Y . Vardi. DPMC: weighted model counting by dynamic programming on project-join trees. In Helmut Simonis, editor, Principles and Practice of Constraint Programming - 26th International Conference, CP 2020, Louvain-la-Neuve, Belgium, S...

    2020 doi

  3. [11]

    Meel, Roger Paredes, and Moshe Y

    Leonardo Due ˜nas-Osorio, Kuldeep S. Meel, Roger Paredes, and Moshe Y . Vardi. Counting-based reliability estimation for power-transmission grids. In Satinder Singh and Shaul Markovitch, ed- itors, Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence, Feb...

    2017 doi

  4. [12]

    An improved gpu-based SAT model counter

    Johannes Klaus Fichte, Markus Hecher, and Markus Zisser. An improved gpu-based SAT model counter. In Thomas Schiex and Simon de Givry, editors, Principles and Practice of Constraint Programming - 25th International Conference, CP 2019, Stamford, CT, USA, September 30 - October...

    2019 doi

  5. [13]

    Exploiting database management systems and treewidth for counting

    Johannes Klaus Fichte, Markus Hecher, Patrick Thier, and Stefan Woltran. Exploiting database management systems and treewidth for counting. Theory Pract. Log. Program. , 22(1):128–157,

  6. [14]

    The silent (r)evolution of SAT

    Johannes Klaus Fichte, Daniel Le Berre, Markus Hecher, and Stefan Szeider. The silent (r)evolution of SAT. Commun. ACM, 66(6):64–72, 2023. doi: 10.1145/3560469. URL https://doi.org/10.1145/ 3560469

    2023 doi

  7. [15]

    Solving projected model counting by utilizing treewidth and its limits

    Johannes Klaus Fichte, Markus Hecher, Michael Morak, Patrick Thier, and Stefan Woltran. Solving projected model counting by utilizing treewidth and its limits. Artif. Intell., 314:103810, 2023. doi: 10.1016/J.ARTINT.2022.103810. URL https://doi.org/10.1016/j.artint.2022.103810

    2023

  8. [16]

    Fomin and Dieter Kratsch

    Fedor V . Fomin and Dieter Kratsch. Exact Exponential Algorithms . Texts in Theoretical Com- puter Science. An EATCS Series. Springer, 2010. ISBN 978-3-642-16532-0. doi: 10.1007/ 978-3-642-16533-7. URL https://doi.org/10.1007/978-3-642-16533-7

    2010 doi

  9. [17]

    Fomin, Serge Gaspers, Saket Saurabh, and Alexey A

    Fedor V . Fomin, Serge Gaspers, Saket Saurabh, and Alexey A. Stepanov. On two techniques of combining branching and treewidth. Algorithmica, 54(2):181–207, 2009. doi: 10.1007/ S00453-007-9133-3. URL https://doi.org/10.1007/s00453-007-9133-3

    2009 doi

  10. [18]

    Serge Gaspers and Gregory B. Sorkin. A universally fastest algorithm for max 2-sat, max 2-csp, and everything in between. In Claire Mathieu, editor, Proceedings of the Twentieth Annual ACM- SIAM Symposium on Discrete Algorithms, SODA 2009, New York, NY, USA, January 4-6, 2009 ...

    2009 doi

  11. [19]

    Gomes, Ashish Sabharwal, and Bart Selman

    Carla P. Gomes, Ashish Sabharwal, and Bart Selman. Model counting. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition , volume 336 of Frontiers in Artificial Intelligence and Applications , pages 993–1014. IOS Press,

  12. [20]

    Taming high treewidth with abstraction, nested dynamic programming, and database technology

    Markus Hecher, Patrick Thier, and Stefan Woltran. Taming high treewidth with abstraction, nested dynamic programming, and database technology. In Luca Pulina and Martina Seidl, editors,Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference...

    2020 doi

  13. [21]

    On the complexity of k-SAT

    Russell Impagliazzo and Ramamohan Paturi. On the complexity of k-SAT. J. Comput. Syst. Sci., 62(2):367–375, 2001. doi: 10.1006/jcss.2000.1727

    2001

  14. [22]

    CNF satisfiability test by counting and polynomial average time

    Kazuo Iwama. CNF satisfiability test by counting and polynomial average time. SIAM J. Comput., 18(2):385–391, 1989. doi: 10.1137/0218026. URL https://doi.org/10.1137/0218026

    1989 doi

  15. [23]

    Integrating tree decompositions into decision heuris- tics of propositional model counters (short paper)

    Tuukka Korhonen and Matti J ¨arvisalo. Integrating tree decompositions into decision heuris- tics of propositional model counters (short paper). In Laurent D. Michel, editor, 27th Interna- tional Conference on Principles and Practice of Constraint Programming, CP 2021, Montpel...

    2021 doi

  16. [24]

    New upper bound for the #3-sat problem

    Konstantin Kutzkov. New upper bound for the #3-sat problem. Inf. Process. Lett. , 105(1):1–5,

  17. [25]

    URL https://doi.org/10.3233/FAIA201009

    doi: 10.3233/FAIA201009. URL https://doi.org/10.3233/FAIA201009

    doi

  18. [26]

    Shrotri, Kuldeep S

    Nina Narodytska, Aditya A. Shrotri, Kuldeep S. Meel, Alexey Ignatiev, and Jo ˜ao Marques-Silva. Assessing heuristic machine learning explanations with model counting. In Mikol´as Janota and Inˆes Lynce, editors, Theory and Applications of Satisfiability Testing - SAT 2019 - 22...

    2019 doi

  19. [27]

    On the hardness of approximate reasoning

    Dan Roth. On the hardness of approximate reasoning. Artif. Intell., 82(1-2):273–302, 1996. doi: 10.1016/0004-3702(94)00092-1. URL https://doi.org/10.1016/0004-3702(94)00092-1

    1996 doi

  20. [28]

    Algorithms for propositional model counting

    Marko Samer and Stefan Szeider. Algorithms for propositional model counting. J. Discrete Al- gorithms, 8(1):50–64, 2010. doi: 10.1016/J.JDA.2009.06.002. URL https://doi.org/10.1016/j.jda. 2009.06.002

    2010 doi

  21. [29]

    Tian Sang, Paul Beame, and Henry A. Kautz. Performing bayesian inference by weighted model counting. In Manuela M. Veloso and Subbarao Kambhampati, editors, Proceedings, The Twentieth National Conference on Artificial Intelligence and the Seventeenth Innovative Applications of...

    2005

  22. [30]

    Leslie G. Valiant. The complexity of computing the permanent. Theor. Comput. Sci., 8:189–201,

  23. [31]

    A tighter bound for counting max-weight solutions to 2sat instances

    Magnus Wahlstr ¨om. A tighter bound for counting max-weight solutions to 2sat instances. In Martin Grohe and Rolf Niedermeier, editors, Parameterized and Exact Computation, Third International 18 Workshop, IWPEC 2008, Victoria, Canada, May 14-16, 2008. Proceedings, volume 5018...

    2008 doi

  24. [32]

    Lozinskii

    Eliezer L. Lozinskii. Counting propositional models. Inf. Process. Lett., 41(6):327–332, 1992. doi: 10.1016/0020-0190(92)90160-W. URL https://doi.org/10.1016/0020-0190(92)90160-W

    1992 doi

  25. [33]

    Number of models and satisfiability of sets of clauses

    Wenhui Zhang. Number of models and satisfiability of sets of clauses. Theor. Comput. Sci., 155(1): 277–288, 1996. doi: 10.1016/0304-3975(95)00144-1. URL https://doi.org/10.1016/0304-3975(95) 00144-1

    1996 doi

  26. [34]

    at least two clauses are removed when we assign a value to x

    Junping Zhou, Minghao Yin, and Chunguang Zhou. New worst-case upper bound for #2-sat and #3- sat with the number of clauses as the parameter. In Maria Fox and David Poole, editors,Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2010, Atlanta, ...

    2010 doi

  27. [40]

    An exact maxsat algorithm: Further observations and further improvements

    Mingyu Xiao. An exact maxsat algorithm: Further observations and further improvements. In Luc De Raedt, editor, Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI 2022, Vienna, Austria, 23-29 July 2022, pages 1887–1893. ijcai.org, ...

    2022 doi

  28. [1971]

    doi: 10.1145/800157.805047. 16

  29. [1979]

    URL https://doi.org/10.1016/0304-3975(79)90044-6

    doi: 10.1016/0304-3975(79)90044-6. URL https://doi.org/10.1016/0304-3975(79)90044-6

    doi

  30. [2003]

    URL https://doi.org/10.1109/SFCS.2003.1238208

    doi: 10.1109/SFCS.2003.1238208. URL https://doi.org/10.1109/SFCS.2003.1238208

    2003 arXiv

  31. [2005]

    URL https://doi.org/10.1016/j.jalgor.2004.06.008

    doi: 10.1016/J.JALGOR.2004.06.008. URL https://doi.org/10.1016/j.jalgor.2004.06.008

    2004 doi

  32. [2007]

    URL https://doi.org/10.1016/j.ipl.2007.06.017

    doi: 10.1016/J.IPL.2007.06.017. URL https://doi.org/10.1016/j.ipl.2007.06.017

    2007 doi

  33. [2021]

    URL https://doi.org/10.3233/FAIA336

    doi: 10.3233/FAIA336. URL https://doi.org/10.3233/FAIA336

    doi

  34. [2022]

    URL https://doi.org/10.1017/S147106842100003X

    doi: 10.1017/S147106842100003X. URL https://doi.org/10.1017/S147106842100003X

    doi

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.