pith. sign in

arxiv: 2606.02143 · v1 · pith:UD3XQL4Tnew · submitted 2026-06-01 · 💻 cs.LO

On Proof Systems for #QBF

Sravanthi Chede , Leroy Chew , Vaibhav Krishan , Anil Shukla This is my paper

Pith reviewed 2026-06-28 11:42 UTC · model grok-4.3

classification 💻 cs.LO
keywords #QBFproof systemsSkolem functionsQ-MICEMICEcountingquantified Boolean formulasXOR-PAIRS
0
0 comments X

The pith

A line-based proof system Q-MICE counts Skolem functions for quantified Boolean formulas and certifies counts for formulas hard for expansion systems.

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

The paper develops proof systems that certify the number of winning strategies, or Skolem functions, for quantified Boolean formulas. Expansion-based systems are shown to suffer inherent structural weaknesses that produce lower bounds. In their place the authors define Q-MICE, whose inference rules mirror the line-based MICE system for ordinary #SAT but are adapted to the quantified setting. The new system yields short proofs for the quantified version of the XOR-PAIRS formula, a family known to be hard for MICE, and thereby separates Q-MICE from all expansion-based #QBF systems.

Core claim

We propose a #QBF proof system that we call Q-MICE, which consists of sound inference rules for computing and certifying the #QBF solution, similar to the line-based #SAT proof system MICE. To demonstrate the strength of Q-MICE, we present various upper bounds, such as the quantified version of the propositional XOR-PAIRS formula, which are known to be hard for MICE. Consequently, we also separate Q-MICE from the expansion-based #QBF proof systems.

What carries the argument

Q-MICE, a line-based calculus whose inference rules compute and certify the number of Skolem functions for a QBF.

If this is right

  • Q-MICE supplies short certificates for the number of Skolem functions on quantified XOR-PAIRS instances.
  • Any expansion-based #QBF proof system requires super-polynomial size on the same quantified XOR-PAIRS family.
  • Q-MICE can be used to certify the output of #QBF solvers that return solution counts.
  • The separation shows that line-based counting rules are strictly stronger than expansion rules for #QBF.

Where Pith is reading between the lines

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

  • An implementation of Q-MICE could serve as a certificate checker inside existing #QBF solvers.
  • The same style of line-based rules might extend to counting problems over other quantified logics.
  • If the rules admit efficient verification, Q-MICE proofs could be checked in polynomial time relative to proof length.

Load-bearing premise

The inference rules of Q-MICE are sound with respect to the semantics of counting Skolem functions for QBFs.

What would settle it

A concrete QBF together with a claimed count on which Q-MICE produces a derivation whose final number differs from the actual number of Skolem functions.

read the original abstract

For a quantified Boolean formula (QBF), the problem of computing the number of winning strategies is known as the #QBF problem. This problem is considered harder than the analogous #SAT problem. Recently, important proof systems for QBFs and #SAT have been studied. By extending the ideas from both fields, we show that it is possible to design proof systems for #QBF. Such proof systems are important not only for advancing the theory of #QBF but also for certifying and designing better #QBF solvers, an area that is still in its early stages. In this paper, we explore #QBF proof systems to count the number of Skolem functions. Apart from a naive system, we study #QBF systems based on the expansion rule of universal variables in QBFs. We observe that these systems have inherent structural weaknesses that lead to lower bounds. As an alternative, we propose a #QBF proof system that we call Q-MICE, which consists of sound inference rules for computing and certifying the #QBF solution, similar to the line-based #SAT proof system MICE. To demonstrate the strength of Q-MICE, we present various upper bounds, such as the quantified version of the propositional XOR-PAIRS formula, which are known to be hard for MICE. Consequently, we also separate Q-MICE from the expansion-based #QBF proof systems.

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 / 1 minor

Summary. The paper introduces proof systems for #QBF, the problem of counting winning strategies (Skolem functions) for quantified Boolean formulas. It analyzes a naive system and expansion-based systems, identifies structural weaknesses leading to lower bounds, and proposes Q-MICE, a line-based system extending the MICE proof system from #SAT. The central claims are that Q-MICE rules are sound and that Q-MICE yields upper bounds (e.g., on the quantified XOR-PAIRS formula, known to be hard for MICE) that separate it from both MICE and expansion-based #QBF systems.

Significance. If the soundness argument and separation results hold, the work contributes to the theory of #QBF proof systems and may support certification of #QBF solvers, an area noted as early-stage. The explicit comparison to MICE and expansion systems provides a clear benchmark for assessing relative strength.

major comments (2)
  1. [Abstract] Abstract (paragraph on Q-MICE definition): the claim that the inference rules of Q-MICE are sound with respect to the semantics of counting Skolem functions is load-bearing for all subsequent upper-bound and separation results, yet the abstract supplies no derivation, proof sketch, or error analysis; the full manuscript must contain an explicit soundness argument (e.g., induction over rule applications) for this to be verifiable.
  2. [Abstract] Abstract (final paragraph): the asserted upper bounds on the quantified XOR-PAIRS formula and the consequent separation from MICE and expansion-based systems are presented without any concrete construction, size bound, or comparison table; these claims are central to demonstrating strength but cannot be assessed without the specific proof or size analysis in the main body.
minor comments (1)
  1. The abstract refers to 'various upper bounds' but details only one example; an enumerated list or table of the claimed bounds would improve readability.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the detailed comments. We clarify that the full manuscript contains the explicit arguments requested; the abstract is a high-level summary only. We respond point by point below.

read point-by-point responses

  1. Referee: [Abstract] Abstract (paragraph on Q-MICE definition): the claim that the inference rules of Q-MICE are sound with respect to the semantics of counting Skolem functions is load-bearing for all subsequent upper-bound and separation results, yet the abstract supplies no derivation, proof sketch, or error analysis; the full manuscript must contain an explicit soundness argument (e.g., induction over rule applications) for this to be verifiable.

    Authors: The full manuscript provides an explicit soundness proof for the Q-MICE rules in Section 3. Soundness is established by induction on the number of rule applications: the base case is the empty proof (counting the single trivial Skolem function), and each inference rule is shown to preserve the exact number of Skolem functions satisfying the formula. The induction hypothesis is applied directly to the premises, with the quantified-variable handling following from the definition of Skolem functions. This argument is self-contained and does not rely on external results beyond standard QBF semantics. revision: no

  2. Referee: [Abstract] Abstract (final paragraph): the asserted upper bounds on the quantified XOR-PAIRS formula and the consequent separation from MICE and expansion-based systems are presented without any concrete construction, size bound, or comparison table; these claims are central to demonstrating strength but cannot be assessed without the specific proof or size analysis in the main body.

    Authors: Section 4 of the manuscript contains the explicit Q-MICE proof for the quantified XOR-PAIRS formula, including the line-by-line derivation, the polynomial-size bound (O(n^3) lines), and the separation argument. The proof exploits the line-based counting rules of Q-MICE to avoid the exponential blow-up that occurs under expansion. A comparison table (Table 1) lists the known lower bounds for MICE and the two expansion-based systems against the Q-MICE upper bound. All size analyses and rule applications are given in full. revision: no

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper defines Q-MICE as a new line-based proof system extending MICE to #QBF, proves soundness of its inference rules directly against the standard semantics of counting Skolem functions, and derives upper bounds and separations from expansion-based systems via explicit rule applications on concrete formulas such as quantified XOR-PAIRS. No equations reduce a claimed result to a fitted parameter or self-referential definition; no load-bearing uniqueness theorem or ansatz is imported via self-citation; all separations rest on independent syntactic arguments rather than renaming or constructionally forced predictions. The derivation chain is therefore self-contained against external semantic benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Paper rests on standard definitions of QBF semantics, Skolem functions, and the MICE system; no free parameters or invented entities introduced in the abstract.

axioms (1)
  • domain assumption Inference rules of Q-MICE are sound for counting Skolem functions
    Invoked when defining the system and claiming upper bounds (abstract).

pith-pipeline@v0.9.1-grok · 5786 in / 1256 out tokens · 20669 ms · 2026-06-28T11:42:23.110805+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

29 extracted references · 7 canonical work pages

  1. [1]

    Olaf Beyersdorff and Tim Hoffmann and Luc Nicolas Spachmann , title =. J. Satisf. Boolean Model. Comput. , volume =. 2024 , doi =

    2024

  2. [2]

    Ladner , title =

    Richard E. Ladner , title =. 1989 , doi =

    1989

  3. [3]

    Journal of the ACM , volume =

    John Alan Robinson , title =. Journal of the ACM , volume =. 1963 , pages =. doi:10.1145/321160.321166 , timestamp =

    work page doi:10.1145/321160.321166 1963

  4. [4]

    Proofs for Propositional Model Counting , booktitle =

    Johannes Klaus Fichte and Markus Hecher and Valentin Roland , editor =. Proofs for Propositional Model Counting , booktitle =. 2022 , doi =

    2022

  5. [5]

    Valiant , title =

    L. Valient , title =. Theor. Comput. Sci. , volume =. 1979 , timestamp =. doi:10.1016/0304-3975(79)90044-6 , _bib2doi_selected =

    work page doi:10.1016/0304-3975(79)90044-6 1979

  6. [6]

    Knowledge Compilation Languages as Proof Systems , booktitle =

    Florent Capelli , editor =. Knowledge Compilation Languages as Proof Systems , booktitle =. 2019 , doi =

    2019

  7. [7]

    1879 , publisher =

    Gottlob Frege , title =. 1879 , publisher =

  8. [8]

    Counting

    Andreas Plank and Sibylle M. Counting. Constraints An Int. J. , volume =. 2024 , doi =

    2024

  9. [9]

    OuterCount:

    Ankit Shukla and Sibylle M. OuterCount:. Intelligent Computer Mathematics - 15th International Conference,. 2022 , doi =

    2022

  10. [10]

    Logic, Automata, and Computational Complexity: The Works of Stephen A

    The relative efficiency of propositional proof systems , author =. Logic, Automata, and Computational Complexity: The Works of Stephen A. Cook , pages =. 2023 , publisher =. doi:10.1145/3588287.3588299 , timestamp =

    work page doi:10.1145/3588287.3588299 2023

  11. [11]

    Extended Resolution Simulates

    Benjamin Kiesl and Adri. Extended Resolution Simulates. Automated Reasoning - 9th International Joint Conference,. 2018 , doi =

    2018

  12. [12]

    Bounded arithmetic, propositional logic, and complexity theory , series =

    Jan Kraj. Bounded arithmetic, propositional logic, and complexity theory , series =. 1995 , isbn =

    1995

  13. [13]

    Singh, Nuclear Data Sheets forA=172, Nucl

    Hans. Resolution for Quantified. Information and Computation , volume =. doi:10.1006/INCO.1995.1025 , year =

    work page doi:10.1006/inco.1995.1025 1995

  14. [14]

    Bryant and Wojciech Nawrocki and Jeremy Avigad and Marijn J

    Randal E. Bryant and Wojciech Nawrocki and Jeremy Avigad and Marijn J. H. Heule , title =. J. Artif. Intell. Res. , volume =. 2025 , url =. doi:10.1613/jair.1.15958 , timestamp =

    work page doi:10.1613/jair.1.15958 2025

  15. [15]

    Marijn J. H. Heule and Martina Seidl and Armin Biere , title =. J. Autom. Reason. , volume =. 2017 , doi =

    2017

  16. [16]

    Olaf Beyersdorff and Joshua Blinkhorn and Meena Mahajan , title =. J. Autom. Reason. , volume =. doi:10.1007/S10817-020-09560-1 , year =

    work page doi:10.1007/s10817-020-09560-1

  17. [17]

    Frege Systems for

    Olaf Beyersdorff and Ilario Bonacina and Leroy Chew and J. Frege Systems for. J. 2020 , doi =

    2020

  18. [18]

    Circuits, Proofs and Propositional Model Counting , booktitle =

    Sravanthi Chede and Leroy Chew and Anil Shukla , editor =. Circuits, Proofs and Propositional Model Counting , booktitle =. 2024 , doi =

    2024

  19. [19]

    Mathematics for Computation (M4C) , chapter =

    Olaf Beyersdorff , title =. Mathematics for Computation (M4C) , chapter =. 2023 , doi =

    2023

  20. [20]

    The Relative Strength of

    Olaf Beyersdorff and Johannes Klaus Fichte and Markus Hecher and Tim Hoffmann and Kaspar Kasche , editor =. The Relative Strength of. 27th International Conference on Theory and Applications of Satisfiability Testing,. 2024 , doi =

    2024

  21. [21]

    Improved affine encryption algorithm for color images using

    Ayseg. Improved affine encryption algorithm for color images using. Multim. Tools Appl. , volume =. 2023 , doi =

    2023

  22. [22]

    2009 , timestamp =

    Sanjeev Arora and Boaz Barak , title =. 2009 , timestamp =

    2009

  23. [23]

    Cook and Robert A

    Stephen A. Cook and Robert A. Reckhow , title =. J. Symb. Log. , year =. doi:10.2307/2273702 , number =

    work page doi:10.2307/2273702

  24. [24]

    1991 , doi =

    Seinosuke Toda , title =. 1991 , doi =

    1991

  25. [25]

    Expansion-based

    Mikol. Expansion-based. Theor. Comput. Sci. , volume =. 2015 , doi =

    2015

  26. [26]

    A Top-Down Tree Model Counter for Quantified Boolean Formulas , booktitle =

    Florent Capelli and Jean. A Top-Down Tree Model Counter for Quantified Boolean Formulas , booktitle =. 2024 , url =

    2024

  27. [27]

    Meel , editor =

    Arijit Shaw and Brendan Juba and Kuldeep S. Meel , editor =. An Approximate Skolem Function Counter , booktitle =. 2024 , doi =

    2024

  28. [28]

    Genuine Lower Bounds for

    Olaf Beyersdorff and Joshua Blinkhorn , editor =. Genuine Lower Bounds for. 35th Symposium on Theoretical Aspects of Computer Science,. 2018 , doi =

    2018

  29. [29]

    G. S. Tseitin , title =. Studies in Mathematics and Mathematical Logic, Part II , editor =. 1970 , note =

    1970