Pith. sign in

REVIEW 3 major objections 5 minor 61 references

#P is Sandwiched by One and Two #2DNF Calls: Is Subtraction Stronger Than We Thought?

T0 review · 3 major / 5 minor · reviewed 2026-08-07 · deepseek-v4-flash

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

Pith's one-line read The paper proves that subtracting the model counts of two 2CNF or 2DNF formulas captures gapP, placing #P strictly between one and two calls to a #2DNF oracle.

desk verdict Main reduction is clever, but the central correctness proof contains a false inclusion-exclusion identity; results unproven as written. read the letter →

arxiv 2506.06716 v1 pith:X3UQX6TJ submitted 2025-06-07 cs.CC cs.DMcs.DScs.LOmath.CO

Max Bannach , Erik D. Demaine , Timothy Gomez , Markus Hecher This is my paper
classification cs.CCcs.DMcs.DScs.LOmath.CO MSC 68Q1568Q1768Q25
keywords countingcomplexity#PgapP#2SAT#2DNFspanLsparsificationSETH
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

The paper proves that counting the satisfying assignments of a 2DNF formula is, by itself, weak, but subtracting the counts of two such formulas is very strong: the difference captures gapP, the class of all functions obtainable as accepting minus rejecting paths of a nondeterministic polynomial-time machine. Since #P sits strictly inside gapP, this places #P strictly between one and two calls to a #2DNF oracle, a gap that would collapse NL and NP or UP and SPP if closed. The construction is a direct, linear-time/logspace reduction from #SAT that encodes inclusion-exclusion and cancels all errors through a symmetry between the two formulas. The same machinery yields a single #2DNF call plus AC0 or TC0 postprocessing that captures gapP and, consequently, the polynomial hierarchy.

What carries the argument

The load-bearing object is the 'rogue model': in the two constructed formulas ψ1 and ψ2, every satisfying assignment that does not correspond to a genuine model of φ is paired by an explicit bijection, the symmetric rogue model construction, which flips the even/odd parity bits along the unique lexicographically first root-to-leaf path containing a rogue node. Because each rogue model of ψ1 maps to exactly one rogue model of ψ2 and vice versa, subtracting the two counts cancels all errors and leaves #(φ). The reduction is guided by a labeled tree decomposition, which is also what gives the additive parameter preservation for treewidth, bandwidth, and their incidence variants.

What would settle it

Run the construction on a small CNF whose tree decomposition includes a join node and an empty-label node, then brute-force count models of the two output formulas: any instance with #(ψ1) − #(ψ2) different from #(φ) falsifies the rogue-model bijection and with it the central claim.

Watch

Extended reading notes

Core claim

The central discovery is a characterization: gapP = [#2SAT−#2SAT]^log = [#IMPL2SAT−#IMPL2SAT]^log = [#0,1-2DNF−#0,1-2DNF]^log = [#2DNF−#2DNF]^log = [#MON2SAT−#MON2SAT]^log = [#MON2DNF−#MON2DNF]^log = spanL−spanL, and hence #P is strictly sandwiched between one and two #2DNF oracle calls. The proof rests on a new reduction from #SAT to two 2CNF formulas ψ1 and ψ2 with #(φ) = #(ψ1) − #(ψ2), computable in linear time or logspace and preserving treewidth, incidence treewidth, bandwidth, and incidence bandwidth up to small additive constants. The reduction works even for monotone 2CNF/2DNF and for cubic bipartite implication formulas, so subtraction compensates both for missing negations and for missing long clauses. As corollaries the paper derives sparsification for #2SAT and #2DNF, an O($2^{{itw(φ)}}$|φ|) algorithm for #SAT, SETH-tight lower bounds, and refined Toda-type inclusions PH ⊆ [#MON2SAT]^log_TC0 = [#MON2DNF]^log_TC0 and PH ⊆ [#IMPL2SAT]^log_AC0.

Load-bearing premise

The paper's central equality #(φ) = #(ψ1) − #(ψ2) collapses if the symmetric pairing of rogue models fails for any labeled tree-decomposition node, in particular for join nodes or nodes with empty labels; the entire sandwich and gapP characterization rests on that bijection.

Editorial extensions

If this is right

  • If correct, #P is strictly contained between one and two #2DNF oracle calls under standard assumptions; closing the gap would show NL = NP or UP = SPP.
  • A single subtraction exactly compensates for the absence of negation: monotone #2SAT and #2DNF differences still capture gapP.
  • One #2DNF call plus AC0 or TC0 postprocessing captures gapP and the polynomial hierarchy, giving a logspace-computable refinement of Toda's theorem.
  • Linear-time, parameter-preserving reduction yields an O(2^{itw(φ)}|φ|) algorithm for #SAT and SETH-tight lower bounds for #2SAT fragments.
  • Any d-CNF can be sparsified into a sum of differences of sparse 2-CNF (or 2-DNF) model counts, extending sparsification to the k=2 case.

Reading between the lines

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

  • Beyond the paper, the rogue-model symmetry is a general template: any counting problem with a tree-decomposition-guided reduction and a parity-like error structure may admit a two-call subtraction characterization, even where negation is absent.
  • Because the two formulas differ by at most one literal or variable occurrence, the result suggests that 'subtraction strength' is measured by how much symmetry a fragment can support; testing fragments between MON2SAT and full 2SAT would map that trade-off.
  • The AC0/TC0 postprocessing results suggest a hierarchy of single-call characterizations: weaker fragments need stronger postprocessing; quantifying this trade-off for fragments such as 1DNF or HORN2SAT could refine the boundary of Toda's theorem.
  • The conjecture that [FP−#MON2SAT]^log is strictly weaker than [#MON2SAT−#MON2SAT]^log, if settled, would show that both calls must be to the same counting oracle; an FP oracle cannot replace one of them.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 5 minor

Summary. The paper presents a reduction from #SAT to the difference of two #2SAT (and #2DNF) oracle calls, claiming that #(φ) = #(ψ1) − #(ψ2) for 2CNF formulas ψ1, ψ2 computable in linear time and logspace. From this main lemma it derives a characterization of gapP as the logspace closure of differences of #2SAT/#2DNF calls, strict separation results for #P, refined Toda-style theorems with AC0/TC0 postprocessing, a sparsification lemma for #2SAT/#2DNF, and parameterized lower bounds under (S)ETH. The proof of the main lemma rests on an inclusion-exclusion argument (Proposition 31) and a bijection between 'rogue models' of the two constructed formulas (Lemmas 28–30).

Significance. If the central lemma holds, the results are strong and novel: they would place #P strictly between one and two #2DNF calls, give a clean gapP characterization, improve Toda's theorem in a logspace-many-one framework, and yield linear-time parameter-preserving reductions with only additive treewidth overhead. The paper's constructive reductions and the explicit examples are valuable. However, the correctness proof as written contains a false inclusion-exclusion identity; until that is repaired, the main theorems are unproven. The flaw is concrete and appears in a load-bearing proposition, so the manuscript needs substantial revision.

major comments (3)
  1. [Appendix 9, Proposition 31] The stated inclusion-exclusion identity is incorrect. For a fixed assignment M that falsifies exactly k clauses of φ, the contribution to the sum Σ_{0≤nc≤|φ|, M does not satisfy ≥nc clauses} (−1)^nc is Σ_{nc=0}^{k} (−1)^nc, which equals 1 if k is even and 0 if k is odd, not the indicator of k=0. Consequently the identities #(φ)=|E|−|O| and #(φ)=#(ψ1)−#(ψ2) do not follow. A concrete counterexample is φ=(x)∧(x), where #(φ)=1 but the E/O expression counts the falsifying assignment x=false as contributing 1, giving 2. The standard inclusion-exclusion identity uses subsets S of falsified clauses with weight (−1)^|S| and hence binomial coefficients; the paper's sum over thresholds 'at least nc' is not equivalent. This invalidates the proof of Lemma 4 and, with it, Theorems 3, 7, 12–14, Corollaries 5, 15, 18, and Corollary 26. The construction's non-rogue models may well encode subsets correctly, but the proof as written must be replaced by a correct subset-based argument.
  2. [Appendix 9, Lemmas 28–30 and Definitions 22–23] The rogue-model bijection is not rigorously established for all tree-decomposition node types. Lemma 28's case analysis is incomplete: in Case (iii), the situation where exactly one of c. or c̄. lies in M is not discussed, and such a model may still be rogue at t via condition (ii) or (iv). For join nodes, the clauses (9)–(12) depend on two child nodes simultaneously, but Definition 23 flips parities only along a single root-to-leaf path; it is not shown that flipping along that path preserves satisfaction of the join-node clauses involving the other child. The proof also relies on an informal 'lexicographically smallest path' argument that is not made precise for general trees with empty-label and join nodes. A complete proof must handle all combinations of conditions (i)–(iv) and all node types, including the cubic-bipartite variants in Appendix 9-C.
  3. [Proposition 31 and Lemma 30] The relationship between 'nc' in the inclusion-exclusion sum and 'nc' in Lemma 30 is ambiguous. In Proposition 31 the summation variable ranges over thresholds ('M does not satisfy ≥nc clauses'), while in Lemma 30(1) nc is defined as the number of c. variables set true in a model M, and Lemma 30(2) asserts that nc is odd exactly for models of ψ2. These are different uses of the same symbol. To make the proof valid, the authors must define E and O as sets of non-rogue models of ψ1 and ψ2, respectively, and then prove that |E|−|O| equals the number of satisfying assignments of φ, e.g., by showing that non-rogue models of ψ1 (resp. ψ2) correspond bijectively to pairs (β,S) where S is an even-sized (resp. odd-sized) subset of clauses falsified by β, with each subset counted exactly once. The current text does not supply such a bijection.
minor comments (5)
  1. [Section IV, Example 21] The reported counts #(ψ1)=204,452 and #(ψ2)=204,450 are not derived; a brief explanation or a small verification table would help the reader confirm the subtraction yields #(φ)=2.
  2. [Definitions 22, 35, 41] The notation for the two clause-auxiliary variables is inconsistent across the paper: the main text uses 'c.' and 'c̄.', while some appendix definitions write 'c.' and 'c̄.' with different spacing. Please standardize the symbols.
  3. [Appendix 10, proof of Theorem 7] The switch and monswitch constructions are described tersely; for instance the claimed equality #(α)=#(ψ1)+#(ψ'2)+#(β)+1 for monswitch requires a case analysis of the four settings of the switch variables, which should be spelled out.
  4. [Appendix 9-A, Lemma 34] The bandwidth-preservation proof is hard to follow and appears to introduce many auxiliary batches and implications; a cleaner formal argument with explicit bounds for the dilation is needed.
  5. [Corollary 26] The sparsification statement says 'there exists t∈N such that in time t·poly(n)', but the dependency of t on k and the precise construction of the γ_i^1, γ_i^2 formulas is not fully specified; the proof refers only to modifications of a cited lemma.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the reduction is self-contained and its reuse of the paper's own Lemma 4 is ordinary proof composition, not input-equivalent reasoning.

full rationale

The paper's central derivation builds ψ1 and ψ2 from a CNF φ via an explicit literal-level construction (Equations (1)-(12), monotone variant (13)-(19), cubic/bipartite variant (20)-(21)) and proves #(φ)=#(ψ1)-#(ψ2) through the rogue-model bijection (Definitions 22-23, Lemmas 28-30). None of these components is defined in terms of the target equality, nor is any parameter fitted to a subset of data and then renamed a prediction; the construction is uniform and parameter-free. Theorem 7 and the gapP characterization reuse Lemma 4 and Theorem 3 internally, but that is a normal proof chain: Lemma 4 is established independently of the class-characterization claim. Citations to prior work (Valiant's #P-completeness chain, Alvarez-Jenner's spanL, Fenner-Fortnow-Kurtz's gapP = #P - #P, Toda's theorem) are external evidence and are not used to smuggle in the paper's own conclusion. The apparent issue in Proposition 31's inclusion-exclusion sum is a correctness or proof-completeness concern about how non-rogue assignments are counted, not a circularity: the formula is asserted to follow from inclusion-exclusion, and if that assertion is wrong the proof fails, but it does not reduce the theorem to its own assumptions. Therefore the circularity score is 0.

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

The paper introduces no fitted parameters. It relies on standard complexity-theoretic facts and hypotheses (gapP = #P − #P, spanL properties, Toda's theorem ingredients, SETH/ETH, AC0/TC0 facts). The only invented notion is the 'rogue model' used inside the correctness proof, which is a mathematical device rather than a postulated physical entity.

assumptions (7)
  • standard math gapP = {f - g : f,g ∈ #P} (Fenner et al. [20, Prop 3.5])
    Used in Theorem 7 proof to reduce gapP to #P − #P.
  • domain assumption #DNF ∈ spanL and spanL ⊆ #P (Alvarez and Jenner [2])
    Used for the sandwich corollaries and Theorem 7's trivial containment.
  • domain assumption spanL ⊊ #P unless NL = NP ([2, Prop 4.10], [19])
    Provides the strict separation in Corollary 8.
  • standard math Valiant's Cook-Levin reduction is parsimonious and logspace, #P = [#3SAT]^log [44]
    Used in Theorem 7 to translate #P oracle calls to #3SAT.
  • domain assumption Almost simplicial rule: contracting a degree-2 vertex in a tree decomposition does not increase width beyond 2 [14]
    Used in Corollary 15 to bound tw(ψ_i) ≤ itw(φ)+15.
  • domain assumption SETH and ETH imply lower bounds for s-SAT [30]
    Used for Theorems 16 and 17.
  • standard math Division is TC0-complete; AC0 ⊊ TC0 [27,25]
    Used to justify postprocessing classes in Theorems 12-14.
invented entities (1)
  • rogue models
    purpose: Classes of satisfying assignments to ψ1/ψ2 that violate the intended parity counts; they are cancelled by subtracting the two oracle calls via a constructed bijection.
    A proof-internal concept. Its defining property (bijection between rogue models of ψ1 and ψ2) is the key technical lemma, but it has no external falsifiable handle beyond the proof itself.

how reviews work

0 comments
Cite this review

Pith. "Pith review of #P is Sandwiched by One and Two #2DNF Calls: Is Subtraction Stronger Than We Thought?." pith.science (2026). https://pith.science/paper/X3UQX6TJ

@misc{pith2026250606716,
  author       = {Pith},
  title        = {Pith review of: #P is Sandwiched by One and Two #2DNF Calls: Is Subtraction Stronger Than We Thought?},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/X3UQX6TJ}},
  note         = {Machine review of arXiv:2506.06716}
}
abstract

The canonical class in the realm of counting complexity is #P. It is well known that the problem of counting the models of a propositional formula in disjunctive normal form (#DNF) is complete for #P under Turing reductions. On the other hand, #DNF $\in$ spanL and spanL $\not\subseteq$ #P unless NL = NP. Hence, the class of functions logspace-reducible to #DNF is a strict subset of #P under plausible complexity-theoretic assumptions. By contrast, we show that two calls to a (restricted) #2DNF oracle suffice to capture gapP, namely, that the logspace many-one closure of the subtraction between the results of two #2DNF calls is gapP. Because #P $\not\subseteq$ gapP, #P is strictly contained between one and two #2DNF oracle calls. Surprisingly, the propositional formulas needed in both calls are linear-time computable, and the reduction preserves interesting structural as well as symmetry properties, leading to algorithmic applications. We show that a single subtraction suffices to compensate for the absence of negation while still capturing gapP, i.e., our results carry over to the monotone fragments of #2SAT and #2DNF. Since our reduction is linear-time, it preserves sparsity and, as a consequence we obtain a sparsification lemma for both #2SAT and #2DNF. This has only been known for kSAT with k $\geq$ 3 and respective counting versions. We further show that both #2DNF calls can be combined into a single call if we allow a little postprocessing (computable by AC0- or TC0-circuits). Consequently, we derive refined versions of Toda's Theorem: PH $\subseteq$ [#MON2SAT]$^{log}_{TC0}$ = [#MON2DNF]$^{log}_{TC0}$ and PH $\subseteq$ [#IMPL2SAT]$^{log}_{AC0}$. Our route to these results is via structure-aware reductions that preserve parameters like treewidth up to an additive overhead. The absence of multiplicative overhead indeed yields parameterized SETH-tight lower bounds.

Figures

Figures reproduced from arXiv: 2506.06716 by the authors.

Figure 1
Figure 1. Overview of complexity classes considered in this paper. An arrow [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 3
Figure 3. Illustration of our reduction that is guided along any given tree decom [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figure 4
Figure 4. An illustration of the four different non-rogue cases per tree decomposition node t (with child node t ′ ), based on the single choice of variable in set {o1t, o2t, e1t, e2t}. Indeed, Equations (3)–(6) model all four potential cases, but also add many more rogue models we eliminate by subtraction. This works due to symmetry (see Definitions 22, 23). o1t2 → et1 o1t2 → c2. o1t2 → ot2 o1t3 → et2 o1t3 → c3. o1t3 → ot3 (… view at source ↗
Figures from the paper (1 more)
Figure 5
Figure 5. Figure 5: Abstract visualization of the symmetric rogue model and its construc [PITH_FULL_IMAGE:figures/full_fig_p009_5.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

61 extracted references · 47 canonical work pages

  1. [1]

    Mix Barrington, and Huong L ˆeThanh

    Eric Allender, Samir Datta, Andris Ambainis, David A. Mix Barrington, and Huong L ˆeThanh. Bounded depth arithmetic circuits: Counting and closure. In Jir´ı Wiedermann, Peter van Emde Boas, and Mogens Nielsen, editors,Automata, Languages and Programming, pages 149–158, Berlin, Heidelberg, 1999. Springer Berlin Heidelberg

    work page 1999

  2. [2]

    A very hard log-space counting class.Theor

    Carme `Alvarez and Birgit Jenner. A very hard log-space counting class.Theor. Comput. Sci., 107(1):3–30, 1993.doi:10.1016/ 0304-3975(93)90252-O

    work page 1993

  3. [3]

    Completeness, approximability and exponential time results for counting problems with easy decision version.Theoretical Computer Science, 915:55–73, 2022

    Antonis Antonopoulos, Eleni Bakali, Aggeliki Chalki, Aris Pagourtzis, Petros Pantavos, and Stathis Zachos. Completeness, approximability and exponential time results for counting problems with easy decision version.Theoretical Computer Science, 915:55–73, 2022

    work page 2022

  4. [4]

    #NFA admits an FPRAS: efficient enumeration, counting, and uniform generation for logspace classes.J

    Marcelo Arenas, Luis Alberto Croquevielle, Rajesh Jayaram, and Cris- tian Riveros. #NFA admits an FPRAS: efficient enumeration, counting, and uniform generation for logspace classes.J. ACM, 68(6):48:1–48:40, 2021.doi:10.1145/3477045

    doi:10.1145/3477045 2021

  5. [5]

    Graph isomorphism is in spp.Information and Computation, 204(5):835–852, 2006

    V Arvind and Piyush P Kurur. Graph isomorphism is in spp.Information and Computation, 204(5):835–852, 2006

    work page 2006

  6. [6]

    Guest column: A panorama of counting problems the decision version of which is in p3.ACM SIGACT News, 53(3):46–68, 2022

    Eleni Bakali, Aggeliki Chalki, Andreas G ¨obel, Aris Pagourtzis, and Stathis Zachos. Guest column: A panorama of counting problems the decision version of which is in p3.ACM SIGACT News, 53(3):46–68, 2022

    work page 2022

  7. [7]

    On the power of counting the total number of computation paths of nptms

    Eleni Bakali, Aggeliki Chalki, Sotiris Kanellopoulos, Aris Pagourtzis, and Stathis Zachos. On the power of counting the total number of computation paths of nptms. InAnnual Conference on Theory and Applications of Models of Computation, pages 209–220. Springer, 2024

    work page 2024

  8. [8]

    Characterizations and approximability of hard counting classes below

    Eleni Bakali, Aggeliki Chalki, and Aris Pagourtzis. Characterizations and approximability of hard counting classes below. InInternational Conference on Theory and Applications of Models of Computation, pages 251–262. Springer, 2020

    work page 2020

Show all 61 references
  1. [9]

    Counting classes: Thresholds, parity, mods, and fewness

    Richard Beigel, John Gill, and Ulrich Hertramp. Counting classes: Thresholds, parity, mods, and fewness. InAnnual Symposium on Theoretical Aspects of Computer Science, pages 49–57. Springer, 1990

    1990

  2. [10]

    Spielman

    Richard Beigel, Nick Reingold, and Daniel A. Spielman. PP is closed under intersection.J. Comput. Syst. Sci., 50(2):191–202, 1995. URL: https://doi.org/10.1006/jcss.1995.1017,doi:10.1006/JCSS.1995. 1017

    1995

  3. [11]

    Handbook of Satisfiability, Second Edition

    Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability, Second Edition. IOS Press, 2021

    2021

  4. [12]

    Bodlaender, Paul S

    Hans L. Bodlaender, Paul S. Bonsma, and Daniel Lokshtanov. The fine details of fast dynamic programming over tree decompositions. In8th In- ternational Symposium on Parameterized and Exact Computation (IPEC 2013), pages 41–53, 2013.doi:10.1007/978-3-319-03898-8\ _5

    2013 doi

  5. [13]

    Bodlaender and Ton Kloks

    Hans L. Bodlaender and Ton Kloks. Efficient and constructive algo- rithms for the pathwidth and treewidth of graphs.Journal of Algorithms, 21(2):358–402, 1996

    1996

  6. [14]

    Bodlaender, Arie M

    Hans L. Bodlaender, Arie M. C. A. Koster, Frank van den Eijkhof, and Linda C. van der Gaag. Pre-processing for triangulation of probabilistic networks. In17th Conference in Uncertainty in Artificial Intelligence (UAI 2001), pages 32–39, 2001

    2001

  7. [15]

    Block interpolation: A framework for tight exponential-time counting complexity.Inf

    Radu Curticapean. Block interpolation: A framework for tight exponential-time counting complexity.Inf. Comput., 261:265–280, 2018. URL: https://doi.org/10.1016/j.ic.2018.02.008,doi:10.1016/J.IC. 2018.02.008

    2018 doi

  8. [16]

    Counting mod- els for 2SAT and 3SAT formulae.Theor

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

    2005 doi

  9. [17]

    Exponential Time Complexity of the Permanent and the Tutte Polynomial.ACM Trans

    Holger Dell, Thore Husfeldt, D ´aniel Marx, Nina Taslaman, and Martin Wahlen. Exponential Time Complexity of the Permanent and the Tutte Polynomial.ACM Trans. Algorithms, 10(4):21:1–21:32, 2014.doi: 10.1145/2635812

    2014 doi

  10. [18]

    Subtractive reductions and complete problems for counting complexity classes

    Arnaud Durand, Miki Hermann, and Phokion G Kolaitis. Subtractive reductions and complete problems for counting complexity classes. Theoretical Computer Science, 340(3):496–513, 2005

    2005

  11. [19]

    Dyer, Leslie Ann Goldberg, Catherine S

    Martin E. Dyer, Leslie Ann Goldberg, Catherine S. Greenhill, and Mark Jerrum. The Relative Complexity of Approximate Counting Problems.Algorithmica, 38(3):471–500, 2004. URL: https://doi.org/10. 1007/s00453-003-1073-y,doi:10.1007/S00453-003-1073-Y

    2004 doi

  12. [20]

    Fenner, Lance Fortnow, and Stuart A

    Stephen A. Fenner, Lance Fortnow, and Stuart A. Kurtz. Gap-definable counting classes.J. Comput. Syst. Sci., 48(1):116–148, 1994.doi: 10.1016/S0022-0000(05)80024-8

    1994 doi

  13. [21]

    The model counting competition 2020.ACM J

    Johannes Klaus Fichte, Markus Hecher, and Florim Hamiti. The model counting competition 2020.ACM J. Exp. Algorithmics, 26:13:1–13:26, 2021.doi:10.1145/3459080

    2020 doi

  14. [22]

    Counting List Homomorphisms from Graphs of Bounded Treewidth: Tight Complexity Bounds.ACM Trans

    Jacob Focke, D ´aniel Marx, and Pawel Rzazewski. Counting List Homomorphisms from Graphs of Bounded Treewidth: Tight Complexity Bounds.ACM Trans. Algorithms, 20(2):11, 2024.doi:10.1145/ 3640814

    2024

  15. [23]

    PP is closed under truth-table reductions.Inf

    Lance Fortnow and Nick Reingold. PP is closed under truth-table reductions.Inf. Comput., 124(1):1–6, 1996. URL: https://doi.org/10. 1006/inco.1996.0001,doi:10.1006/INCO.1996.0001

    1996

  16. [24]

    Synthesis Lectures on Artificial Intelligence and Machine Learning

    Martin Gebser, Roland Kaminski, Benjamin Kaufmann, and Torsten Schaub.Answer Set Solving in Practice. Synthesis Lectures on Artificial Intelligence and Machine Learning. Morgan & Claypool Publishers, 2012.doi:10.2200/S00457ED1V01Y201211AIM019

    2012 doi

  17. [25]

    Almost optimal lower bounds for small depth circuits

    Johan H ˚astad. Almost optimal lower bounds for small depth circuits. In Juris Hartmanis, editor,18th Annual ACM Symposium on Theory of Computing (STOC’86), pages 6–20. ACM, 1986.doi:10.1145/ 12130.12132

    1986

  18. [26]

    Relations among mod-classes.Theoretical Computer Science, 74(3):325–328, 1990

    Ulrich Hertrampf. Relations among mod-classes.Theoretical Computer Science, 74(3):325–328, 1990

    1990

  19. [27]

    Mix Barrington

    William Hesse, Eric Allender, and David A. Mix Barrington. Uniform constant-depth threshold circuits for division and iterated multiplica- tion.J. Comput. Syst. Sci., 65(4):695–716, 2002.doi:10.1016/ S0022-0000(02)00025-9

    2002

  20. [28]

    The complexity of the inertia and some closure properties of gapl

    Thanh Minh Hoang and Thomas Thierauf. The complexity of the inertia and some closure properties of gapl. In20th Annual IEEE Conference on Computational Complexity (CCC 2005), pages 28–37. IEEE Computer Society, 2005.doi:10.1109/CCC.2005.28

    2005 doi

  21. [29]

    Nondeterministic space is closed under complemen- tation.SIAM J

    Neil Immerman. Nondeterministic space is closed under complemen- tation.SIAM J. Comput., 17(5):935–938, 1988.doi:10.1137/ 0217058

    1988

  22. [30]

    On the complexity of k- SAT.Journal of Computer and System Sciences, 62(2):367–375, 2001

    Russell Impagliazzo and Ramamohan Paturi. On the complexity of k- SAT.Journal of Computer and System Sciences, 62(2):367–375, 2001

    2001

  23. [31]

    Some (in)translatability results for normal logic pro- grams and propositional theories.J

    Tomi Janhunen. Some (in)translatability results for normal logic pro- grams and propositional theories.J. Appl. Non Class. Logics, 16(1- 2):35–86, 2006. URL: https://doi.org/10.3166/jancl.16.35-86,doi: 10.3166/JANCL.16.35-86

    2006 doi

  24. [32]

    Picturing counting reductions with the ZH-calculus

    Tuomas Laakkonen, Konstantinos Meichanetzidis, and John van de Wetering. Picturing counting reductions with the ZH-calculus. In20th International Conference on Quantum Physics and Logic (QPL 2023), pages 89–113, 2023.doi:10.4204/EPTCS.384.6

    2023 doi

  25. [33]

    A faster fpras for# nfa.Proceedings of the ACM on Management of Data, 2(2):1–22, 2024

    Kuldeep S Meel, Sourav Chakraborty, and Umang Mathur. A faster fpras for# nfa.Proceedings of the ACM on Management of Data, 2(2):1–22, 2024

    2024

  26. [34]

    On closure properties of #P in the context of PF◦#P.J

    Mitsunori Ogihara, Thomas Thierauf, Seinosuke Toda, and Osamu Watanabe. On closure properties of #P in the context of PF◦#P.J. Comput. Syst. Sci., 53(2):171–179, 1996. URL: https://doi.org/10.1006/ jcss.1996.0059,doi:10.1006/JCSS.1996.0059

    1996

  27. [35]

    Hemachandra

    Mitsunori Ogiwara and Lane A. Hemachandra. A complexity theory for feasible closure properties.J. Comput. Syst. Sci., 46(3):295–325, 1993. doi:10.1016/0022-0000(93)90006-I

    1993 doi

  28. [36]

    The complexity of counting functions with easy decision version

    Aris Pagourtzis and Stathis Zachos. The complexity of counting functions with easy decision version. InInternational Symposium on Mathematical Foundations of Computer Science, pages 741–752. Springer, 2006

    2006

  29. [37]

    Two remarks on the power of counting

    Christos H Papadimitriou and Stathis K Zachos. Two remarks on the power of counting. InTheoretical Computer Science: 6th Gl-Conference Dortmund, January 5–7, 1983, pages 269–275. Springer, 1982

    1983

  30. [38]

    Algorithms for propositional model counting.J

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

    2010

  31. [39]

    A faster algorithm for propo- sitional model counting parameterized by incidence treewidth

    Friedrich Slivovsky and Stefan Szeider. A faster algorithm for propo- sitional model counting parameterized by incidence treewidth. In 23rd International Conference on the Theory and Applications of Satisfiability Testing (SAT 2020), volume 12178 ofLecture Notes in Computer Sc...

    2020

  32. [40]

    Computational transition at the uniqueness threshold

    Allan Sly. Computational transition at the uniqueness threshold. In2010 IEEE 51st Annual Symposium on Foundations of Computer Science, pages 287–296. IEEE, 2010

    2010

  33. [41]

    On closure properties of GapP.Comput

    Thomas Thierauf, Seinosuke Toda, and Osamu Watanabe. On closure properties of GapP.Comput. Complex., 4:242–261, 1994.doi:10. 1007/BF01206638

    1994

  34. [42]

    PP is as hard as the polynomial-time hierarchy.SIAM J

    Seinosuke Toda. PP is as hard as the polynomial-time hierarchy.SIAM J. Comput., 20(5):865–877, 1991.doi:10.1137/0220053

    1991 doi

  35. [43]

    Craig A. Tovey. A simplified NP-complete satisfiability prob- lem.Discret. Appl. Math., 8(1):85–89, 1984.doi:10.1016/ 0166-218X(84)90081-7

    1984

  36. [44]

    Leslie G. Valiant. The complexity of computing the permanent.Theor. Comput. Sci., 8:189–201, 1979.doi:10.1016/0304-3975(79) 90044-6

    1979 doi

  37. [45]

    Leslie G. Valiant. The complexity of enumeration and reliability problems.SIAM J. Comput., 8(3):410–421, 1979.doi:10.1137/ 0208032

    1979

  38. [46]

    Valiant and Vijay V

    Leslie G. Valiant and Vijay V . Vazirani. NP is as easy as detecting unique solutions.Theor. Comput. Sci., 47(3):85–93, 1986.doi:10. 1016/0304-3975(86)90135-0. APPENDIX

    1986

  39. [47]

    The symmetric rogue modelM ′ ofMis a satisfying assignment ofψ 2

    PROOF OF THEMAINLEMMA Lemma 28(Well-Definedness).Letφbe aCNF,T be a tree decomposition of it, andMbe a satisfying assignment ofψ 1 that is rogue. The symmetric rogue modelM ′ ofMis a satisfying assignment ofψ 2. Vice versa, the result holds if roles ofMandM ′ are swapped. Proo...

  40. [48]

    Definition 36(Symmetric Rogue Model for Monotony)

    The construction of the symmetric rogue model works analogously as in Definition 23, where instead ofxwe use xand instead ofo1 t,o2 t,e1 t,e2 t we put o1t, o2t, e1t, e2t, respectively. Definition 36(Symmetric Rogue Model for Monotony). LetMbe a model of a formulaφ ′ withφ ′ ⊇R...

  41. [49]

    Vice versa, the result holds if roles ofMandM ′ are swapped. Proof.LetMbe rogue at a nodetand assume that (1) there is no indirect ancestor node oft(e.g., parent node) such thatMis rogue at this node and that (2)tis on the lexicographic smallest root-to-leaf path ofT. Sotis th...

  42. [50]

    Lemma 38.Letφbe aCNF,Tbe a fully labeled tree decomposition of it, andMbe a satisfying assignment ofψ ′ 1 that is rogue

    As for Lemma 28, the roles ofMandM ′ can be switched by symmetry. Lemma 38.Letφbe aCNF,Tbe a fully labeled tree decomposition of it, andMbe a satisfying assignment ofψ ′ 1 that is rogue. Then, (I) a modelMofψ ′ 1 is rogue at a nodetiff the symmetric rogue modelM ′ ofψ ′ 2 is r...

  43. [51]

    In order to show that(I)M ′ =f(M)is also rogue att ′, lett ⋆ be the node ofTsuch thatMis rogue att ⋆ withM not being rogue at an ancestor oft ⋆

    SupposeMis rogue at a nodet ′ ofT. In order to show that(I)M ′ =f(M)is also rogue att ′, lett ⋆ be the node ofTsuch thatMis rogue att ⋆ withM not being rogue at an ancestor oft ⋆. We distinguish the following cases. Caset ′ is an ancestor oft ⋆.By constructionMis not rogue att...

  44. [52]

    gapP⊆[#2SAT−#2SAT] log

    PROOFS FORNEWCHARACTERIZATION OFGAPP Theorem 7(Characterization of GapP).gapP= = [#2SAT−#2SAT] log = [#IMPL2SAT−#IMPL2SAT] log = [#0,1-2DNF−#0,1-2DNF] log = [#2DNF−#2DNF] log = [#DNF−#DNF] log = [#MON2SAT−#MON2SAT] log = [#MON2DNF−#MON2DNF] log = spanL−spanL. The characterizat...

  45. [53]

    ·” to “+

    = (#ψ1 + #ψ ′ 2)−(#ψ 2 + #ψ ′ 1). From this, we con- struct formulaα=ψ 1 ∪ψ ′′ 2, whereψ ′′ 2 is obtained fromψ ′ 2 by replacing every variable with a fresh variable. Analogously, we constructβ=ψ 2 ∪ψ ′′ 1, whereψ ′′ 1 is obtained fromψ ′ 1 by replacing variables with fresh va...

  46. [54]

    [#0,1-2DNF−#0,1-2DNF] log ⊆[#2DNF− #2DNF] log

    = #(¬ψ′)−#(¬ψ) = #(ψ)−#(ψ ′). Case “[#0,1-2DNF−#0,1-2DNF] log ⊆[#2DNF− #2DNF] log”: By definition. Case “[#2DNF−#2DNF] log ⊆[#3DNF−#3DNF] log”: By definition. Case “[#3DNF−#3DNF] log ⊆[#MON2SAT− #MON2SAT] log”: As mentioned above, there is a parsi- monious many-one reduction f...

  47. [55]

    Now, it remains to construct formulasα, α ′ such that#(α)− #(α′) =c= (#(ψ 1) + #(ψ′ 2))−(#(ψ 2) + #(ψ′ 1))

    Then, we have thatc= #(ψ 1)−#(ψ 2)−(#(ψ ′ 1)− #(ψ′ 2)) = (#(ψ1) + #(ψ′ 2))−(#(ψ 2) + #(ψ′ 1)). Now, it remains to construct formulasα, α ′ such that#(α)− #(α′) =c= (#(ψ 1) + #(ψ′ 2))−(#(ψ 2) + #(ψ′ 1)). To this end, we build a formulamonswitch(ι, τ, κ) over three formulasι, τ,...

  48. [56]

    + #(β) + 1 and#(α ′) = #(ψ 2) + #(ψ ′

  49. [57]

    [#MON2SAT−#MON2SAT] log ⊆[#MON2DNF− #MON2DNF] log

    + #(β) + 1, resulting inc= #(α)−#(α ′). Case “[#MON2SAT−#MON2SAT] log ⊆[#MON2DNF− #MON2DNF] log”: Similar to above we assume two for- mulasψandψ ′ inMON2SAT, with the goal of com- puting#(ψ)−#(ψ ′). Then, this equals to2 |vars(ψ)| − #(¬ψ)−(2 |vars(ψ ′)| −#(¬ψ ′)). However, in ...

  50. [58]

    Analogously, we pro- ceed for variablesv j ∈V 2, construct implications incycswitch(V 1, V2), and remove implications from φ2 as above, resulting inφ ′

  51. [59]

    degree3and bipartiteness

    The overall construction preserves max. degree3and bipartiteness

  52. [60]

    gapP⊆[#IMPL2SAT] log AC0

    PROOFS FORA NEWCHARACTERIZATION OFPH Theorem 13.gapP⊆[#IMPL2SAT] log AC0=[#0,1-2DNF] log AC0. This statement holds even if#IMPL2SATis restricted to cubic and bipartite formulas. Proof.“gapP⊆[#IMPL2SAT] log AC0”: In contrast to above, we instead apply Theorems 3 (B) and 7, ther...

  53. [61]

    [#IMPL2SAT] log AC0 = [#0,1-2DNF] log AC0

    Finally, we need to connectBto the switch. Since there are at least3mpossibilities in total (and connecting the variables inV 1 ∪V 2 already used up at most2mof them), this can be achieved by connecting anyb i inBto a variables ∗ j inSthat is not yet connected to a variable in...

Pith tools

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