💻 computer science

On Proof Systems for #QBF

This paper introduces Q-MICE, a novel proof system for #QBF based on sound inference rules that overcomes the structural weaknesses of expansion-based systems and provides upper bounds for formulas known to be hard for existing #SAT solvers.

Original authors: Sravanthi Chede, Leroy Chew, Vaibhav Krishan, Anil Shukla

Published 2026-06-02

📖 4 min read☕ Coffee break read

CC BY 4.0

Original authors: Sravanthi Chede, Leroy Chew, Vaibhav Krishan, Anil Shukla

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are playing a complex game of chess against a very tricky opponent. In this game, you (the "Existential" player) want to win, and your opponent (the "Universal" player) wants to stop you. The game has a twist: your opponent gets to make moves first, and you have to have a plan that works no matter what they do.

In computer science, this game is called a QBF (Quantified Boolean Formula). But this paper isn't just asking, "Can you win?" It's asking a much harder question: "Exactly how many different winning plans do you have?"

This counting problem is called #QBF. It's like trying to count every single possible way you could win a game of chess against a specific opponent, where your strategy must adapt to every single move they could make.

The Problem: Counting is Hard

The authors explain that counting these winning plans is incredibly difficult.

The Naive Way: Imagine trying to list every single winning plan one by one, write it down, and then check if it's unique. If there are billions of plans, this takes forever. If there are trillions, it's impossible.
The "Expansion" Way: Another method tries to simplify the game by pretending the opponent has already made all their possible moves at once. This turns the game into a simpler version, but the list of moves becomes so huge (exponentially huge) that the paper gets crushed under its own weight before it can finish counting.

The Solution: Q-MICE (The Smart Calculator)

The paper introduces a new tool called Q-MICE. Think of Q-MICE not as a person listing every single plan, but as a smart calculator that uses a set of clever shortcuts (inference rules) to count the plans without listing them all.

Here is how Q-MICE works, using a construction analogy:

The Blueprint (Axiom Rule): Instead of building the whole house at once, Q-MICE looks at small, manageable sections of the blueprint. It asks, "If the opponent plays this specific move, how many ways can I win?" It calculates this for small pieces and writes down the number.
Merging Rooms (Composition Rules): Imagine you have counted the ways to win in the kitchen and the ways to win in the living room. Q-MICE has a rule that says, "If these two rooms are separate, just add the numbers together." It can also merge strategies that are almost the same, saving time.
Rejoining the Branches (Join Rule): Sometimes, the game splits into two paths based on the opponent's first move (e.g., they play "White" or "Black"). Q-MICE calculates the winning plans for the "White" path and the "Black" path separately. Then, it multiplies the results to get the total for the whole game, realizing that the paths eventually come back together.

Why is Q-MICE Better?

The authors prove that Q-MICE is much faster and more efficient than the old methods for certain types of games.

The "XOR-PAIRS" Game: They created a specific type of game (based on a logic puzzle called XOR-PAIRS) that is known to be a nightmare for other counting tools. For the old "Expansion" method, solving this game would require a list of plans so long it would stretch across the universe. For Q-MICE, the solution is short and sweet, like a single page of notes.
The "Indexed Affine" Game: They created another game that acts like a simple encryption code. The old methods would take exponential time (a time so long it's practically infinite) to count the plans. Q-MICE solves it in linear time (a time that grows slowly and steadily, like counting steps).

The Big Takeaway

The paper shows that while counting winning strategies in these complex logic games is theoretically very hard, we can build a "proof system" (a set of rules for a computer) that does it efficiently for many important cases.

Q-MICE is like a master architect who doesn't need to count every single brick in a castle to know how many bricks were used. Instead, they look at the patterns, the repeating sections, and the structure to calculate the total instantly. This proves that we can design better software to solve these hard counting problems, moving us past the limitations of simply trying to list every possibility.

Title: On Proof Systems for #QBF

Problem Statement
The paper addresses the #QBF problem, which involves computing the number of winning strategies for the existential player in a Quantified Boolean Formula (QBF). This problem is identified as #PSPACE-complete, making it computationally harder than the analogous #SAT problem (model counting for propositional formulas), where the number of solutions is at most exponential. In contrast, the number of winning strategies in #QBF can be doubly exponential. While proof systems for #SAT (e.g., KCPS, CPOG, CLIP, MICE) and QBF (e.g., Q-Res, ∀Exp) have been studied, there was a lack of dedicated proof systems for the general #QBF problem capable of certifying the count of winning strategies. Existing solvers like d4-QBF and qCounter exist but lack a formalized proof complexity framework for certification.

Methodology
The authors extend concepts from both QBF proof systems and #SAT proof systems to design new proof systems for #QBF. They explore three distinct approaches:

Naive System: A rudimentary system that enumerates all $k$ winning strategies. It certifies the count by proving the correctness of each strategy (via tautology proofs of Skolem functions), proving the distinctness of strategies (via witness assignments), and proving the non-existence of any other strategies (via a false QBF encoding). The authors note this system suffers from trivial lower bounds when the number of strategies is doubly exponential.
Expansion-based System (∀Exp+MICE): This approach adapts the ∀-expansion rule used in QBF solving. It semantically expands the QBF over all possible assignments to universal variables, transforming the #QBF problem into a #SAT problem. The resulting CNF is then processed using the #SAT proof system MICE. The authors argue that this system inherently requires exponential size relative to the number of universal variables because it must expand all universal assignments to preserve the model count.
Line-based System (Q-MICE): The primary contribution is the proposal of Q-MICE (Quantified Model-counting Induction by Claim Extension). Inspired by the MICE system for #SAT, Q-MICE is a line-based proof system where each line is a claim of the form $(Q.F, A, c)$ $(Q . F, A, c)$ .
- $Q.F$ : A true QBF.
- $A$ : A partial strategy consisting of Skolem functions for a subset of existential variables.
- $c$ : The number of ways to extend $A$ into complete winning strategies.
- Inference Rules: Q-MICE utilizes three core rules:
  - Axiom Rule: Derives claims for restricted QBFs where the matrix is a tautology, allowing direct combinatorial counting of extensions.
  - Composition Rules: Allow combining or simplifying claims. Composition-a sums distinct complete strategies; Composition-b drops strategy restrictions when uniqueness is proven; Composition-c combines claims where strategies differ only on specific variables, provided an "absence of models" proof certifies no other strategies exist.
  - Join Rule: Combines two claims that differ only by a restriction on a universal variable, multiplying their counts, provided the structure of the assignment tree allows it (path graphs).

Key Contributions and Results

Formalization of Q-MICE: The paper defines Q-MICE and proves it is sound and complete (Theorem 16). It is polynomial-time verifiable.
Exponential Separation: The authors demonstrate that Q-MICE is exponentially stronger than both the naive system and the ∀Exp+MICE system (Theorem 17).
- XOR-PAIRS Family: They introduce a quantified version of the propositional XOR-PAIRS formula. While this family requires super-polynomial (exponential) proofs in ∀Exp+MICE due to the need to expand universal variables, Q-MICE provides a constant-length, polynomial-size proof by utilizing the Axiom and Composition-b rules.
- Indexed Affine QBF Family: They construct a family of QBFs representing a simple encryption process. This family has $2^n$ winning strategies, necessitating exponential proofs in both the naive and ∀Exp+MICE systems. Q-MICE handles this with a linear-length, polynomial-size proof by iteratively applying composition and join rules.
Structural Analysis: The paper highlights that expansion-based systems suffer from inherent structural weaknesses (exponential blowup) when dealing with universal variables, whereas Q-MICE interleaves quantifier handling with counting to maintain efficiency.

Significance and Claims
The paper claims that the existence of proof systems like Q-MICE is crucial for advancing the theory of #QBF and for certifying the correctness of #QBF solvers, an area currently in its early stages. By providing a framework to certify model counts without enumerating all strategies, Q-MICE offers a path toward more robust solver verification.

The authors modestly note that while Q-MICE is powerful, it does not yet incorporate the decomposition rules found in state-of-the-art solvers like d4-QBF, though they suggest this could be added as a modular inference rule. They also identify open problems, including establishing genuine lower bounds for Q-MICE (conjecturing that propositional XOR-PAIRS might be hard for it, though this is not yet a proven lower bound) and extending other #SAT proof systems (CPOG, CLIP, KCPS) to the #QBF domain. The paper does not propose new experimental solvers but focuses strictly on the theoretical proof complexity and the separation of these systems.

The Problem: Counting is Hard

The Solution: Q-MICE (The Smart Calculator)

Why is Q-MICE Better?

The Big Takeaway

More like this