Pith. sign in

REVIEW 3 major objections 6 minor 18 references

An Expansion-Based Approach for Quantified Integer Programming

T0 review · 3 major / 6 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 A counterexample-guided expansion solver for quantified integer programs outperforms search-based solvers on key benchmarks.

desk verdict First expansion-based QIP solver with a genuinely new universal-move encoding, but the optimization pseudocode has a binary-search bug that needs fixing before the paper can be the reference. read the letter →

arxiv 2506.04452 v1 pith:TREWDHE3 submitted 2025-06-04 cs.DM cs.AIcs.LO

Michael Hartisch , Leroy Chew This is my paper
classification cs.DMcs.AIcs.LO MSC 90C1090C27
keywords quantifiedintegerprogrammingexpansion-basedsolvingcounterexample-guidedabstractionrefinementrobustdiscreteoptimizationBooleanformulaslinearmultistageQRandomParity
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

Quantified Integer Programming (QIP) extends quantified Boolean formulas to integer variables and linear constraints, but until now every QIP solver was search-based, explicitly walking the assignment tree in quantifier order. This paper claims that the expansion paradigm, long used in QBF, can be adapted to QIP through Counterexample-Guided Abstraction Refinement (CEGAR). The resulting solver, EQuIPS, iteratively builds a partial expansion of the quantified problem, using integer programming calls to find winning moves and countermoves, and refines the abstraction until a winner is certified. If the claims hold, expansion-based solving is no longer missing from the QIP landscape, and multistage robust discrete linear optimization problems can be handled by a model-and-run solver rather than specialised reformulations.

What carries the argument

The central object is the refinement rule, adapted from QFUN to integer domains: when a candidate move $\tau$ is beaten by a countermove $\mu$ in a subgame $\Phi$, refine adds a new subgame in which the variables after $\mu$ are replaced by annotated copies, such as $Z^{(\mu)}$, and $\mu$ is substituted into the constraint system. The universal-player subroutine wins1 is the other pillar: it encodes 'violate every subgame constraint system' as one integer program using lower-bound vectors $L_l$ and violation-certificate values $r$, with indicator variables forcing at least one violated constraint per subgame. The integer solver supplies the IP oracle, so the proof system underlying refutations is $\forall$Exp+Cutting Planes, whose soundness and completeness for QIP is Theorem 5.

What would settle it

Run EQuIPS on randomly generated small QIP instances with brute-force game-tree verification available: whenever the solver returns $\bot$, independently check that the existential player really wins, and whenever it returns a move, check the universal player has no countermove; any single mismatch, especially on a QRandomParity variant where Problem (2) is feasible but no universal assignment violates every subgame, would disprove Lemma 7 and the wins1 encoding.

Watch

Extended reading notes

Core claim

The paper's central claim is that a QIP can be solved without full expansion by a CEGAR loop in which an abstraction, a multi-game containing only some countermove branches, is refined until its winning move survives all countermoves. The load-bearing subroutine wins1 answers whether a single assignment wins all quantifier-free subgames: for the existential player this is the conjunction of the constraint systems, and for the universal player it is a single integer program that uses indicator variables per subgame and per constraint. The encoding relies on Lemma 2, which states that a rational linear constraint on integer variables is violated by at least $1/d$ where $d$ is the lowest common denominator of the coefficients, making 'violate all systems' representable as an IP. The paper proves soundness of the solver (Lemma 7 for universal-to-existential outcomes, Lemma 8 via the $\forall$Exp+Cutting Planes proof system) and shows experimentally that EQuIPS solves the new QRandomParity benchmark up to $n=1000$ in median 3.44 seconds, while QFUN with CryptoMiniSat times out on all instances at that size, and that EQuIPS solves 465 of the multilevel critical-node instances versus 431 for Yasol.

Load-bearing premise

The method assumes a violated linear constraint on integer variables is always violated by at least the fixed amount $1/d$, where $d$ is the lowest common denominator of the coefficients, so the universal player's goal can be written as a single integer program; if universal variables could vary continuously, no such minimum gap exists and the encoding would not represent the game.

Editorial extensions

If this is right

  • Expansion-based solving is now available for QIP, so instances with few quantifier alternations, where search-based QCDCL-style solvers are weak, have a viable alternative.
  • Linear constraints give EQuIPS an edge over QBF-only expansion solvers: on QRandomParity, modelling XOR relations as linear equalities with auxiliary variables lets the IP solver's aggregation and preprocessing prove infeasibility quickly.
  • Multistage robust discrete linear optimization problems can be solved directly from a QIP formulation containing a universal constraint system, using binary search over the objective value, without dualising or scenario generation.
  • EQuIPS can act as an optimality verifier for search-based solvers such as Yasol, and the hybrid 'Yasol finds, EQuIPS verifies' loop solves more instances than Yasol alone.
  • The approach inherits the known QBF profile of expansion: it excels with few universal levels and struggles when many alternations force near-complete expansion, as the assignment and scheduling test sets show.

Reading between the lines

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

  • Because Lemma 2 only works for rational coefficients on integer variables, the wins1 encoding cannot be lifted to continuous universally quantified variables; a continuous universal player could violate a constraint by an arbitrarily small amount, so the discrete-certificate trick is the real boundary of the method.
  • QRandomParity's linear encoding suggests a reverse transfer: QBF parity instances could be rewritten with pseudo-Boolean constraints and handed to EQuIPS, and any expansion-based QBF solver that learns to aggregate linear constraints may close the gap to CryptoMiniSat-style XOR handling.
  • The learned-constraint experiment, in which 73 constraints slowed the IP solver but 3 hand-picked constraints sped it up, points to a selective clause-transfer problem: deciding which search-solver conflicts to share with the expansion verifier is a tunable optimisation, similar to cutting-plane selection, though the paper only tests one instance.
  • If EQuIPS's scaling on QRandomParity is robust, random reordered parity could become a standard stress test for quantified decision procedures that emphasises arithmetic reasoning over Boolean structure, complementing existing QBF benchmark families.
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 / 6 minor

Summary. The paper introduces EQuIPS, the first expansion-based solver for Quantified Integer Programming (QIP), adapting the CEGAR-style abstraction-refinement ideas of the QBF solvers RAReQS and QFUN. The solver handles bounded integer variables, linear constraints, optional polyhedral uncertainty on universal variables, and a linear objective. The 'wins1' subroutine solves the quantifier-free multi-game via integer programming: for an existential player it solves a single IP, and for a universal player it solves a dedicated IP encoding the violation of every subgame, using a discrete gap lemma (Lemma 2). The paper also contributes a proof system, ∀Exp+Cutting Planes, and uses it to prove soundness of the solver's negative answers (Lemmas 7 and 8). Optimization is addressed by a binary search over the objective value (Algorithm 3) and by a hybrid scheme that combines Yasol with EQuIPS. Experiments on a new QRandomParity benchmark show that EQuIPS scales to n=1000 in median 3.44 seconds while QFUN with CryptoMiniSat times out on all instances at that size, and on the multilevel critical node (MCN) test set EQuIPS solves 465 instances versus 431 for Yasol and 475 for the specialized MCNCR baseline.

Significance. If the technical issues are resolved, this is a meaningful contribution: it fills a real gap in the QIP landscape by providing an expansion-based alternative to search-based solvers, gives a proof-system justification for the approach, introduces a new benchmark (QRandomParity), and shows concrete performance advantages on structured instances. The availability of the solver source code and the use of standard IP oracles are further strengths. However, the paper's optimization claims currently rest on a binary-search pseudocode that is incorrect as written, and the correctness argument for positive answers (returned winning moves) is incomplete. These problems are fixable but they affect load-bearing parts of the paper, especially the MCN experiments.

major comments (3)
  1. [Section 3.5.1, Algorithm 3] The binary search uses the real-valued midpoint z←(LB+UB)/2 and, on a feasible decision problem, sets UB←z. Since c⊤x is integer for every feasible x, the constraint c⊤x≤z is equivalent to c⊤x≤⌊z⌋. Concretely, if LB=0, UB=1 and the optimum is 0, the first midpoint 0.5 is feasible, UB becomes 0.5, and the loop condition UB−LB>0 never becomes false; even with a tolerance, the returned bound need not be the integer optimum z⋆. The pseudocode must use an integer-preserving midpoint (e.g., z←⌊(LB+UB)/2⌋) together with integer updates (UB←z and LB←z+1 are then integral). Because the MCN experiments in Section 5.2 are reported for 'EQuIPS (utilizing binary search)', this issue is load-bearing for the optimization claims.
  2. [Section 3.4, Lemmas 7 and 8] The soundness argument covers only the case in which EQuIPS returns ⊥. The complementary result—that when EQuIPS returns a move τ, that τ is a winning move of the multi-game—is never stated or proved, although Algorithm 1's refinement step (Line 9) and final return (Line 11) depend on it. The missing direction can be supplied by induction on quantifier depth using Lemmas 7 and 8, but as written the correctness of positive answers is an unstated assumption.
  3. [Section 3.1, Algorithm 1] The while loop in Algorithm 1 has no explicit termination proof. A finite-domain argument should be stated: each refinement adds a subgame that makes the previously returned outer assignment τ no longer a winning move of the refined abstraction, and there are only finitely many assignments to the bounded outer variables. Without such an argument, the claim that EQuIPS is a solver (rather than a possibly non-terminating procedure) is incomplete.
minor comments (6)
  1. [Section 2.1, Lemma 2] The notation 'lcd' should be 'lcm' (least common multiple of denominators); the proof of Lemma 2 should define the intended quantity explicitly, since 'lowest common denominator' is not standard for a set of rational numbers.
  2. [Section 3.5.2, Theorem 9] The symbol D in the statement of Theorem 9 is never defined, and the proof's appeal to Yasol's completeness after learning clauses C1...Cn is informal. Please state the theorem with all symbols defined and give a rigorous argument, or remove the theorem if it is not needed for the experimental claims.
  3. [Section 3.3, Algorithm 1] The 'extract' function used in Line 6 is not defined; please state how an assignment over the annotated variables of the abstraction is projected to the outer block variables XXX.
  4. [Section 5.1, Table 1] The entry '3.44/10' in the last column is ambiguous; clarify that the number after the slash is the number of unsolved instances.
  5. [Section 4.1] The sentence 'In particular, tn=sn must be fulfilled' is not self-explanatory; a sentence explaining that the universal variable u forces the two parity chains to take opposite truth values would make the hardness argument clearer.
  6. [Section 5.2] The comparison to MCNCR is against the baseline from [1], not the enhanced techniques from that paper; this limitation should be stated more prominently so that the reader does not overinterpret the 465-vs-475 count.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the paper's derivation chain is self-contained against external benchmarks; the only flagged issue (Algorithm 3's real-valued binary search midpoint) is a correctness flaw in pseudocode, not a circular derivation.

full rationale

The paper's derivation chain is self-contained. Lemma 2 proves a discrete gap for violating rational linear constraints over integer variables, and Problem (2) is constructed directly from that gap, not from any solver output or fitted quantity. Soundness Lemmas 7 and 8 are established by induction against the independently defined QIP game semantics, with base cases reduced to standard integer programming oracle calls whose completeness is cited to the external cutting-planes result [21]. No parameter is fitted to the reported benchmarks, and no prediction is derived from the paper's own outputs: QRandomParity hardness from [17] motivates a benchmark but does not enter the algorithm, correctness proofs, or solver behavior. Self-citations to earlier QIP work (e.g., [24, 40]) and to QFUN [44] provide provenance and algorithmic inspiration, but the expansion rules, wins1 encoding, and refinement step are defined and proven in this paper rather than assumed from those citations. The only notable flaw is that Algorithm 3 updates bounds using z <- (LB+UB)/2 and UB <- z over an integer objective, which can fail to terminate or return a non-integer bound when the optimum is integer; this is a pseudocode/correctness defect, not a circularity, because the procedure is not defined in terms of its own output and the reported MCN experiments do not derive the claimed comparison from a circular calculation. Accordingly, the circularity score is 0.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

No fitted free parameters were identified; the only tunable choices (10^-p violation threshold, existential IP relaxation versus lower bounds in the empty abstraction) are implementation heuristics, not fitted to data. The proof system and encoding rely on standard math plus the QIP domain assumptions listed. No new physical or conceptual entities are postulated; annotated variable copies Z(YYY=mu) are an abstraction artifact with no independent empirical handle.

assumptions (5)
  • standard math Cutting planes proof system is sound and complete for integer programming.
    Invoked in Theorem 5 and Lemma 8 to argue that IP infeasibility answers can be lifted to refutations.
  • domain assumption Every QIP has bounded integer domains, so full expansion is finite and satisfiability-equivalent.
    Used in Theorem 5; if domains were unbounded, the full expansion argument would collapse.
  • domain assumption The universal constraint system is nonempty and independent of existential variables.
    Stated in Section 2.3; required for the polyhedral uncertainty domain definition and for Problem (2) to remain an IP over universal moves only.
  • standard math For rational linear constraints over integer variables, violation has a minimal gap equal to the reciprocal of the least common denominator.
    Lemma 2 in Section 3.2; this is the load-bearing fact for the universal wins1 encoding.
  • ad hoc to paper The refinement rule adds exactly one new subgame per countermove, so the abstraction grows monotonically within the finite expansion tree.
    Termination is not proved explicitly; the finite-domain argument is implicit in the proof sketch of Theorem 5 and in Lemma 7, but the pseudocode does not guard against duplicate subgames.

how reviews work

0 comments
Cite this review

Pith. "Pith review of An Expansion-Based Approach for Quantified Integer Programming." pith.science (2026). https://pith.science/paper/TREWDHE3

@misc{pith2026250604452,
  author       = {Pith},
  title        = {Pith review of: An Expansion-Based Approach for Quantified Integer Programming},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/TREWDHE3}},
  note         = {Machine review of arXiv:2506.04452}
}
read the original abstract

Quantified Integer Programming (QIP) bridges multiple domains by extending Quantified Boolean Formulas (QBF) to incorporate general integer variables and linear constraints while also generalizing Integer Programming through variable quantification. As a special case of Quantified Constraint Satisfaction Problems (QCSP), QIP provides a versatile framework for addressing complex decision-making scenarios. Additionally, the inclusion of a linear objective function enables QIP to effectively model multistage robust discrete linear optimization problems, making it a powerful tool for tackling uncertainty in optimization. While two primary solution paradigms exist for QBF -- search-based and expansion-based approaches -- only search-based methods have been explored for QIP and QCSP. We introduce an expansion-based approach for QIP using Counterexample-Guided Abstraction Refinement (CEGAR), adapting techniques from QBF. We extend this methodology to tackle multistage robust discrete optimization problems with linear constraints and further embed it in an optimization framework, enhancing its applicability. Our experimental results highlight the advantages of this approach, demonstrating superior performance over existing search-based solvers for QIP in specific instances. Furthermore, the ability to model problems using linear constraints enables notable performance gains over state-of-the-art expansion-based solvers for QBF.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

18 extracted references · 16 canonical work pages

  1. [3]

    9 Olaf Beyersdorff, Leroy Chew, Judith Clymo, and Meena Mahajan

    URL: https://doi.org/10.4230/LIPIcs.ITCS.2021.12,doi:10.4230/LIPICS.ITCS.2021.12. 9 Olaf Beyersdorff, Leroy Chew, Judith Clymo, and Meena Mahajan. Short proofs in qbf expansion. InTheory and Applications of Satisfiability Testing–SAT 2019: 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9–12, 2019, Proceedings 22, pages 19–35. Springer,

    work page doi:10.4230/lipics.itcs.2021.12 2021

  2. [8]

    18 Leroy Chew and Marijn JH Heule

    URL:https://ojs.aaai.org/index.php/ AAAI/article/view/28635,doi:10.1609/aaai.v38i8.28635. 18 Leroy Chew and Marijn JH Heule. Sorting parity encodings by reusing variables. InInterna- tional Conference on Theory and Applications of Satisfiability Testing, pages 1–10. Springer,

    doi:10.1609/aaai.v38i8.28635

  3. [10]

    21 Vašek Chvátal.Cutting-plane proofs and the stability number of a graph

    URL:https://doi.org/10.1007/ s10817-024-09707-4,doi:10.1007/S10817-024-09707-4. 21 Vašek Chvátal.Cutting-plane proofs and the stability number of a graph. Inst. für Ökonometrie und Operations Research, Rhein. Friedrich-Wilhelms-Univ.,

    work page doi:10.1007/s10817-024-09707-4

  4. [12]

    uni-siegen.de/handle/ubsi/1705,doi:http://dx.doi.org/10.25819/ubsi/4841

    URL:https://dspace.ub. uni-siegen.de/handle/ubsi/1705,doi:http://dx.doi.org/10.25819/ubsi/4841. 36 Michael Hartisch. Adaptive relaxations for multistage robust optimization. InPacific Rim International Conference on Artificial Intelligence, pages 485–499. Springer,

    work page doi:10.25819/ubsi/4841

  5. [13]

    Quantified integer programs with polyhedral uncertainty set

    37 Michael Hartisch, Thorsten Ederer, Ulf Lorenz, and Jan Wolf. Quantified integer programs with polyhedral uncertainty set. InComputers and Games: 9th International Conference, CG 2016, Leiden, The Netherlands, June 29–July 1, 2016, Revised Selected Papers 9, pages 156–166. Springer,

    work page 2016

  6. [15]

    Hartisch and L

    M. Hartisch and L. Chew 23 39 Michael Hartisch and Ulf Lorenz. A novel application for game tree search-exploiting pruning mechanisms for quantified integer programs. InAdvances in Computer Games: 16th Interna- tional Conference, ACG 2019, Macao, China, August 11–13, 2019, Revised Selected Papers 16, pages 66–78. Springer,

    work page 2019

  7. [16]

    A general model-and-run solver for multistage robust discrete linear optimization

    40 Michael Hartisch and Ulf Lorenz. A general model-and-run solver for multistage robust discrete linear optimization.arXiv preprint arXiv:2210.11132,

    work page Pith review arXiv

  8. [17]

    org/index.php/AAAI/article/view/12208,doi:10.1609/aaai.v32i1.12208

    URL:https://ojs.aaai. org/index.php/AAAI/article/view/12208,doi:10.1609/aaai.v32i1.12208. 45 Florian Lonsing and Uwe Egly. Depqbf 6.0: A search-based qbf solver beyond traditional qcdcl. InAutomated Deduction–CADE 26: 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6–11, 2017, Proceedings, pages 371–384. Springer,

    work page doi:10.1609/aaai.v32i1.12208

Show all 18 references
  1. [18]

    62 Phebe Vayanos, Daniel Kuhn, and Berç Rustem

    URL: https: //ojs.aaai.org/index.php/AAAI/article/view/28654,doi:10.1609/aaai.v38i8.28654. 62 Phebe Vayanos, Daniel Kuhn, and Berç Rustem. A constraint sampling approach for multi- stage robust optimization.Automatica, 48(3):459–471,

    doi

  2. [2003]

    Understanding the relative strength of QBF CDCL solvers and QBF resolution

    8 Olaf Beyersdorff and Benjamin Böhm. Understanding the relative strength of QBF CDCL solvers and QBF resolution. In James R. Lee, editor,12th Innovations in Theoretical Computer Science Conference, ITCS 2021, January 6-8, 2021, Virtual Conference, volume 185 of LIPIcs, pages ...

    2021

  3. [2015]

    QCDCL vs QBF resolution: Further insights

    14 Benjamin Böhm and Olaf Beyersdorff. QCDCL vs QBF resolution: Further insights. In Meena Mahajan and Friedrich Slivovsky, editors,26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4-8, 2023, Alghero, Italy, volume 271 ofLIPIcs...

    2023

  4. [2016]

    Mastering uncertainty: towards robust multistage optimiza- tion with decision dependent uncertainty

    38 Michael Hartisch and Ulf Lorenz. Mastering uncertainty: towards robust multistage optimiza- tion with decision dependent uncertainty. InPRICAI 2019: Trends in Artificial Intelligence: 16th Pacific Rim International Conference on Artificial Intelligence, Cuvu, Yanuca Island,...

    2019

  5. [2018]

    Yasol: an open source solver for quantified mixed integer programs

    24 Thorsten Ederer, Michael Hartisch, Ulf Lorenz, Thomas Opfer, and Jan Wolf. Yasol: an open source solver for quantified mixed integer programs. InAdvances in Computer Games: 15th International Conferences, ACG 2017, Leiden, The Netherlands, July 3–5, 2017, Revised Selected P...

    2017

  6. [2019]

    New resolution-based QBF calculi and their proof complexity.ACM Trans

    10 Olaf Beyersdorff, Leroy Chew, and Mikolás Janota. New resolution-based QBF calculi and their proof complexity.ACM Trans. Comput. Theory, 11(4):26:1–26:42, 2019.doi:10.1145/3352155. 11 Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Po...

    2019 doi

  7. [2020]

    On the complexity of quantified integer programming

    22 An Expansion-Based Approach for Quantified Integer Programming 19 Dmitry Chistikov and Christoph Haase. On the complexity of quantified integer programming. In44th International Colloquium on Automata, Languages, and Programming (ICALP 2017), volume 80, page

    2017

  8. [2021]

    Hartisch and L

    M. Hartisch and L. Chew 21 2 Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, and Clark Barrett. Extending smt solvers to higher-order logic. InAutomated Deduction–CADE 27: 27th Inter- national Conference on Automated Deduction, Natal, Brazil, August 27–30, ...

    2019

  9. [2023]

    15 Hubie Chen

    URL: https://doi.org/10.4230/LIPIcs.SAT.2023.4,doi:10.4230/LIPICS.SAT.2023.4. 15 Hubie Chen. Beyond Q-resolution and prenex form: A proof system for quantified constraint satisfaction.Logical Methods in Computer Science, 10,

    2023 doi

  10. [2024]

    12 Nikolaj Bjørner, Mikolás Janota, and William Klieber

    doi:10.1007/978-3-031-65627-9\_7. 12 Nikolaj Bjørner, Mikolás Janota, and William Klieber. On conflicts and strategies in QBF. In LPAR (short papers), pages 28–41,

    doi

Pith tools

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