arxiv: 2605.04544 · v1 · submitted 2026-05-06 · 💻 cs.CC

Recognition: unknown

Hard CNF Instances for Ideal Proof Systems

Tuomas Hakoniemi , Nutan Limaye , Iddo Tzameret

Authors on Pith no claims yet

Pith reviewed 2026-05-08 15:34 UTC · model grok-4.3

classification 💻 cs.CC

keywords ideal proof systemCNF refutationslower boundsread-once oblivious ABPfeasible interpolationproof complexityNullstellensatz

0 comments

The pith

Certain CNF formulas require superpolynomial roABP size for their refutations in the ideal proof system.

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

The paper establishes lower bounds showing that some CNF formulas encoding propositional contradictions demand large read-once oblivious algebraic branching program size when refuted in the roABP variant of the ideal proof system. Earlier lower bounds applied only to purely algebraic formulas that are not directly propositional, so this closes a gap by handling actual CNF instances used in logic. The argument adapts a rank-based feasible interpolation method: any roABP refutation is decomposed along a variable partition to extract a low-dimensional space of polynomials, from which an interpolating span program is built. If correct, this means algebraic proof systems face concrete size barriers even on Boolean formulas, limiting how efficiently they can certify unsatisfiability in propositional logic.

Core claim

The authors prove that there exist CNF formulas whose refutations in roABP-IPS_LIN require superpolynomial size. They achieve this via a rank-based feasible interpolation argument in which a given roABP refutation is decomposed along a partition of the variables, producing a low-dimensional space of polynomials that yields a correct span-program interpolant. This extends prior degree-based Nullstellensatz results to the setting where refutation size is measured by roABP complexity.

What carries the argument

Rank-based feasible interpolation that decomposes an roABP refutation along a variable partition to extract a low-dimensional polynomial space for constructing a span-program interpolant.

If this is right

Lower bounds now hold for roABP-IPS_LIN on CNF formulas that encode propositional contradictions.
The size measure based on roABP complexity replaces the earlier degree measure from Nullstellensatz refutations.
The interpolation technique reduces the problem of bounding refutation size to the complexity of constructing span-program interpolants.

Where Pith is reading between the lines

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

The same decomposition-plus-interpolation strategy might be adapted to obtain CNF lower bounds in other restricted algebraic proof systems.
If the bounds scale with formula size, they suggest that roABP-IPS cannot efficiently certify all unsatisfiable CNFs even when the formulas are simple.
One could test whether the method yields explicit size lower bounds for concrete families such as pigeonhole or clique formulas.

Load-bearing premise

Any roABP refutation can be decomposed along a variable partition into a low-dimensional space of polynomials from which a correct span-program interpolant can always be constructed.

What would settle it

A concrete small roABP refutation for one of the specific CNF formulas shown to be hard would disprove the lower bound for that instance.

read the original abstract

Since the introduction of the Ideal Proof System (IPS) by Grochow and Pitassi (J. ACM 2018), a substantial body of work has established size lower bounds for IPS and its fragments. In particular, Forbes, Shpilka, Tzameret, and Wigderson (Theory Comput. 2021) developed the main lower-bound frameworks for restricted IPS fragments, namely functional lower bounds and the hard multiples method, while Alekseev, Grigoriev, Hirsch, and Tzameret (SIAM J. Comput. 2024) gave a general template for conditional lower bounds for full IPS. Yet all these lower bounds apply only to purely algebraic formulas over a field, that is, non-Boolean formulas not directly expressible in propositional logic. Proving lower bounds for CNF formulas has therefore remained a central open problem in this line of work. The current work resolves this question for IPS over read-once oblivious algebraic branching programs (roABPs) by proving lower bounds for refutations of CNF formulas in this system. Our approach is a rank-based feasible interpolation argument, following the method of Pudl\'ak and Sgall (Proof Complexity and Feasible Arithmetic 1996) for monotone span programs, in which decomposing a given roABP refutation along a variable partition yields a low-dimensional space of polynomials from which we construct a span-program interpolant. We extend their result from Nullstellensatz refutations measured by degree to Nullstellensatz refutations measured by roABP size (i.e., roABP-IPS$_\text{LIN}$).

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.

Desk Editor's Note private letter to a colleague

This paper closes the CNF lower-bound gap for roABP-IPS by adapting rank-based interpolation from degree to roABP size.

read the letter

The main takeaway is that this work gives the first size lower bounds on roABP-IPS refutations of CNF formulas, resolving the open question left after the algebraic-only results in Forbes et al. and Alekseev et al. They do it by lifting the Pudlak-Sgall rank-based feasible interpolation to work with roABP size instead of degree: any roABP refutation decomposes along a variable partition into a low-dimensional polynomial space, from which a span-program interpolant is built, and then hard multiples or similar constructions produce the CNF instances. That extension is the concrete new piece. It sits cleanly on top of the cited prior frameworks without obvious reinvention. The abstract presents the logic as a direct size analogue of the earlier Nullstellensatz case, which is a reasonable move if the dimension control holds. One soft spot worth checking is exactly how the decomposition controls dimension for roABPs; the read-once oblivious structure might introduce some looseness or extra factors compared with plain degree, and if those factors are not tight the final lower bounds could end up weaker than the high-level claim suggests. No other red flags jump out from the outline. This is for people already working in algebraic proof complexity and IPS fragments. A reader tracking lower-bound techniques for restricted proof systems will find the interpolation carry-over useful. It deserves a serious referee because it targets a stated open problem with a focused technical step rather than a broad survey. I would send it out for review.

Referee Report

0 major / 1 minor

Summary. The manuscript proves lower bounds for refutations of CNF formulas in the roABP-IPS_LIN fragment of the Ideal Proof System. It adapts the rank-based feasible interpolation technique of Pudlák and Sgall by showing that any roABP refutation decomposes along a variable partition into a low-dimensional space of polynomials, from which a correct span-program interpolant is constructed; this extends the prior degree-based Nullstellensatz result to a size measure.

Significance. If the central construction holds, the result is significant: it supplies the first explicit lower bounds for CNF instances in a restricted IPS fragment, closing a gap between algebraic proof systems and propositional logic. The approach reuses an established interpolation framework without introducing free parameters or circularity, and the dimension-control step is presented as the direct size analogue of the degree case.

minor comments (1)

Abstract: the acronym 'roABP-IPS_LIN' appears without a parenthetical gloss or forward reference; a one-sentence definition on first use would improve readability for readers outside the immediate sub-area.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the careful reading of the manuscript and for recommending acceptance. The referee's summary accurately reflects the paper's contribution in extending rank-based feasible interpolation from degree to roABP size for CNF refutations in roABP-IPS_LIN.

Circularity Check

0 steps flagged

Minor self-citation present but derivation remains independent of inputs

full rationale

The paper's central claim is an extension of the external Pudlák-Sgall (1996) rank-based feasible interpolation technique to roABP refutations of CNF formulas, with Forbes et al. (2021) cited only for background frameworks on IPS lower bounds. Although one co-author overlaps with the 2021 citation, the load-bearing step (decomposing roABP refutations into low-dimensional polynomial spaces for span-program interpolants) is presented as a direct adaptation of the 1996 method rather than a reduction to any fitted parameter, self-definition, or unverified self-citation chain. No equations or steps in the provided abstract reduce the result to its own inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The work relies on standard linear-algebra facts for rank arguments and on the correctness of the cited feasible-interpolation template; no free parameters, new entities, or ad-hoc axioms are introduced in the abstract.

axioms (1)

standard math Standard facts from linear algebra over fields (rank, dimension, vector spaces)
Invoked when decomposing the roABP along a variable partition to obtain a low-dimensional polynomial space.

pith-pipeline@v0.9.0 · 5594 in / 1294 out tokens · 68904 ms · 2026-05-08T15:34:18.311809+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

299 extracted references · 70 canonical work pages

[1]

Archive for Mathematical Logic , volume=

Iterated multiplication in VTC 0 , author=. Archive for Mathematical Logic , volume=. 2022 , publisher=

2022
[2]

An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams , journal =

Jan Kraj. An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams , journal =. 2008 , url =. doi:10.2178/JSL/1208358751 , timestamp =

work page doi:10.2178/jsl/1208358751 2008
[3]

CoRR , volume =

Nathan Segerlind , title =. CoRR , volume =. 2007 , url =. cs/0701054 , timestamp =

work page arXiv 2007
[4]

6 Sam Buss, Dmitry Itsykson, Alexander Knop, Artur Riazanov, and Dmitry Sokolov

Sam Buss and Dmitry Itsykson and Alexander Knop and Artur Riazanov and Dmitry Sokolov , title =. 2021 , url =. doi:10.1145/3468855 , timestamp =

work page doi:10.1145/3468855 2021
[5]

Ran Raz and Pierre McKenzie , title =. Comb. , volume =. 1999 , url =. doi:10.1007/S004930050062 , timestamp =

work page doi:10.1007/s004930050062 1999
[6]

Theory Comput

Siu Man Chan and Aaron Potechin , title =. Theory Comput. , volume =. 2014 , url =. doi:10.4086/TOC.2014.V010A015 , timestamp =

work page doi:10.4086/toc.2014.v010a015 2014
[7]

Cook , editor =

Robert Robere and Toniann Pitassi and Benjamin Rossman and Stephen A. Cook , editor =. Exponential Lower Bounds for Monotone Span Programs , booktitle =. 2016 , url =. doi:10.1109/FOCS.2016.51 , timestamp =

work page doi:10.1109/focs.2016.51 2016
[8]

Annals of Pure and Applied Logic , volume=

Short propositional refutations for dense random 3CNF formulas , author=. Annals of Pure and Applied Logic , volume=. 2014 , publisher=

2014
[9]

Garlik, Michal and Gryaznov, Svyatoslav and Hanlin, Ren and Tzameret, Iddo , title =
[10]

Proof complexity , author =
[11]

, title =

Razborov, Alexander A. , title =. Izv. Ross. Akad. Nauk Ser. Mat. , fjournal =
[12]

9th Innovations in Theoretical Computer Science Conference (ITCS 2018) , pages =

Paul Beame and Noah Fleming and Russell Impagliazzo and Antonina Kolokolova and Denis Pankratov and Toniann Pitassi and Robert Robere , title =. 9th Innovations in Theoretical Computer Science Conference (ITCS 2018) , pages =. doi:10.4230/LIPIcs.ITCS.2018.10 , annote =

work page doi:10.4230/lipics.itcs.2018.10 2018
[13]

Hastad , booktitle =

J. Hastad , booktitle =. doi:10.1109/FOCS.2017.18 , url =

work page doi:10.1109/focs.2017.18 2017
[14]

Towards an Understanding of Polynomial Calculus: New Separations and Lower Bounds , booktitle =

Filmus, Yuval and Lauria, Massimo and Mik. Towards an Understanding of Polynomial Calculus: New Separations and Lower Bounds , booktitle =
[15]

Yaroslav Alekseev , title =
[16]

Annals of Pure and Applied Logic (to appear) , year = 2020, note =

Sam Buss and Valentine Kabanets and Antonina Kolokolova and Michal Koucky , title =. Annals of Pure and Applied Logic (to appear) , year = 2020, note =

2020
[17]

A sorting network in bounded arithmetic , journal =

Emil Je. A sorting network in bounded arithmetic , journal =
[18]

Phuong Nguyen , title =
[19]

, year = 2007, booktitle =

Phuong Nguyen and Stephen Cook , title =. , year = 2007, booktitle =

2007
[20]

Logical strength of complexity theory and a formalization of the

J\'. Logical strength of complexity theory and a formalization of the
[21]

Subsystems of Second Order Arithmetic , publisher =

Stephen Simpson , editor =. Subsystems of Second Order Arithmetic , publisher =
[22]

Theory of Computing Systems , year = 2010, month =

Galesi, Nicola and Lauria, Massimo , title =. Theory of Computing Systems , year = 2010, month =. doi:10.1007/s00224-009-9195-5 , url =

work page doi:10.1007/s00224-009-9195-5 2010
[23]

and Steiglitz, Kenneth , title =

Papadimitriou, Christos H. and Steiglitz, Kenneth , title =
[24]

Theory of Linear and Integer Programming , author =
[25]

Handbook on Semidefinite, Conic and Polynomial Optimization , year = 2012, publisher =

Chlamtac, Eden and Tulsiani, Madhur , title =. Handbook on Semidefinite, Conic and Polynomial Optimization , year = 2012, publisher =. doi:10.1007/978-1-4614-0769-0_6 , url =

work page doi:10.1007/978-1-4614-0769-0_6 2012
[26]

Sum-of-squares proofs and the quest toward optimal algorithms , author =
[27]

On the Unique Games Conjecture (Invited Survey) , booktitle =

Khot, Subhash , year = 2010, month = 06, pages =. On the Unique Games Conjecture (Invited Survey) , booktitle =

2010
[28]

Shor, N. Z. , title =. Cybernetics , year = 1987, volume = 23, number = 6, pages =

1987
[29]

Hypercontractive inequalities via SOS, and the Frankl¿Rödl graph , isbn =

Kauers, Manuel and O'Donnell, Ryan and Tan, Li-Yang and Zhou, Yuan , year = 2014, pages =. Hypercontractive inequalities via SOS, and the Frankl¿Rödl graph , isbn =. Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms , doi =

2014
[30]

Marshall, Murray , year = 2008, title =

2008
[31]

Emerging Applications of Algebraic Geometry , year = 2009, publisher =

Laurent, Monique , title =. Emerging Applications of Algebraic Geometry , year = 2009, publisher =

2009
[32]

Linear Programming , year = 1991, publisher =

Karloff, Howard , title =. Linear Programming , year = 1991, publisher =. doi:10.1007/978-0-8176-4844-2_4 , url =

work page doi:10.1007/978-0-8176-4844-2_4 1991
[33]

35th Symposium on Theoretical Aspects of Computer Science (STACS 2018) , pages =

Christoph Berkholz , title =. 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018) , pages =. doi:10.4230/LIPIcs.STACS.2018.11 , annote =

work page doi:10.4230/lipics.stacs.2018.11 2018
[34]

Arvind and Partha Mukhopadhyay and S

V. Arvind and Partha Mukhopadhyay and S. Raja , title =. ArXiV , url =
[35]

ACM SIGLOG News , year = 2015, volume = 2, number = 3, pages =

Jakob Nordstrom , title =. ACM SIGLOG News , year = 2015, volume = 2, number = 3, pages =

2015
[36]

Essential covers of the cube by hyperplanes , journal =
[37]

Ramanujan graphs

Lubotzky, A. and Phillips, R. and Sarnak, P. , title =. Combinatorica , year = 1988, month =. doi:10.1007/BF02126799 , url =

work page doi:10.1007/bf02126799 1988
[38]

Covering the Cube by Affine Hyperplanes , journal =

Alon, Noga and F\". Covering the Cube by Affine Hyperplanes , journal =. doi:10.1006/eujc.1993.1011 , acmid = 156548, publisher =

work page doi:10.1006/eujc.1993.1011 1993
[39]

, editor =

Kaltofen, Erich L. , editor =. Factorization of polynomials given by straight-line programs , booktitle =
[40]

Computational Complexity , volume =

Kabanets, Valentine and Impagliazzo, Russell , title =. ComputationalComplexity , volume = 13, number =. doi:10.1007/s00037-004-0182-6 , note =

work page doi:10.1007/s00037-004-0182-6
[41]

Nisan, Noam and Wigderson, Avi , title =. J. Comput. Syst. Sci. , volume = 49, number = 2, year = 1994, pages =. doi:10.1016/S0022-0000(05)80043-1 , note =

work page doi:10.1016/s0022-0000(05)80043-1 1994
[42]

Proceedings of the Annual ACM Symposium on the Theory of Computing

Impagliazzo, Russell and Wigderson, Avi , title =. Proceedings of the Annual ACM Symposium on the Theory of Computing. doi:10.1145/258533.258590 , missing =

work page doi:10.1145/258533.258590
[43]

, title =

Sudan, Madhu and Trevisan, Luca and Vadhan, Salil P. , title =. J. Comput. Syst. Sci. , volume = 62, number = 2, year = 2001, pages =. doi:10.1006/jcss.2000.1730 , note =

work page doi:10.1006/jcss.2000.1730 2001
[44]

, volume = 39, number = 4, year = 2009, pages =

Dvir, Zeev and Shpilka, Amir and Yehudayoff, Amir , title =. , volume = 39, number = 4, year = 2009, pages =. doi:10.1137/080735850 , note =

work page doi:10.1137/080735850 2009
[45]

doi:10.4230/LIPIcs.CCC.2015.198 , toupdate =

Oliveira, Rafael , title =. doi:10.4230/LIPIcs.CCC.2015.198 , toupdate =

work page doi:10.4230/lipics.ccc.2015.198 2015
[46]

, title =

von zur Gathen, Joachim and Kaltofen, Erich L. , title =. , volume = 31, number = 2, pages =. doi:10.1016/0022-0000(85)90044-3 , note =

work page doi:10.1016/0022-0000(85)90044-3
[47]

doi:10.4230/LIPIcs.APPROX-RANDOM.2015.943 , note =

Volkovich, Ilya , title =. doi:10.4230/LIPIcs.APPROX-RANDOM.2015.943 , note =

work page doi:10.4230/lipics.approx-random.2015.943 2015
[48]

Proceedings of the Annual ACM Symposium on the Theory of Computing

Heintz, Joos and Schnorr, Claus-Peter , title =. Proceedings of the Annual ACM Symposium on the Theory of Computing. doi:10.1145/800141.804674 , missing =

work page doi:10.1145/800141.804674
[49]

doi:10.1007/11590156_6 , missing =

Agrawal, Manindra , title =. doi:10.1007/11590156_6 , missing =

work page doi:10.1007/11590156_6
[50]

doi:10.1007/978-0-387-35651-8 , toupdate =

Cox, David and Little, John and O'Shea, Donal , title =. doi:10.1007/978-0-387-35651-8 , toupdate =

work page doi:10.1007/978-0-387-35651-8
[51]

Cox, David and Little, John and O'Shea, Donal , title =
[52]

, title =

Forbes, Michael A. , title =. IEEE Annual Symposium on Foundations of Computer Science
[53]

Polynomial Identity Testing of Read-Once Oblivious Algebraic Branching Programs , author =
[54]

and Shpilka, Amir , title =

Forbes, Michael A. and Shpilka, Amir , title =. Proceedings of the Annual ACM Symposium on the Theory of Computing. doi:10.1145/2213977.2213995 , note =

work page doi:10.1145/2213977.2213995
[55]

and Shpilka, Amir , title =

Forbes, Michael A. and Shpilka, Amir , title =. doi:10.1007/978-3-642-40328-6_37 , note =

work page doi:10.1007/978-3-642-40328-6_37
[56]

Forbes and Amir Shpilka , title =

Michael A. Forbes and Amir Shpilka , title =. 54th Annual. 2013 , url =. doi:10.1109/FOCS.2013.34 , timestamp =

work page doi:10.1109/focs.2013.34 2013
[57]

Diagonal Circuit Identity Testing and Lower Bounds

Saxena, Nitin. Diagonal Circuit Identity Testing and Lower Bounds. Automata, Languages and Programming. 2008

2008
[58]

Kayal, Neeraj , howpublished =
[59]

Computational Complexity , VOLUME =

Nisan, Noam and Wigderson, Avi , title =. Computational Complexity , volume = 6, number = 3, year = 1996, pages =. doi:10.1007/BF01294256 , note =

work page doi:10.1007/bf01294256 1996
[60]

Electronic Colloquium on Computational Complexity

Kayal, Neeraj , title =. Electronic Colloquium on Computational Complexity
[61]

, volume = 61, month = dec, year = 2014, number = 6, pages =

Gupta, Ankit and Kamath, Pritish and Kayal, Neeraj and Saptharishi, Ramprasad , title =. , volume = 61, month = dec, year = 2014, number = 6, pages =. doi:10.1145/2629541 , note =

work page doi:10.1145/2629541 2014
[62]

Proceedings of the Annual ACM Symposium on the Theory of Computing

Agrawal, Manindra and Saha, Chandan and Saxena, Nitin , title =. Proceedings of the Annual ACM Symposium on the Theory of Computing. doi:10.1145/2488608.2488649 , note =

work page doi:10.1145/2488608.2488649
[63]

Gurjar, Rohit and Korwar, Arpita and Saxena, Nitin and Thierauf, Thomas , title =
[64]

Oliveira, Rafael , howpublished =
[65]

ECCC , volume = 22, pages = 42, year = 2015, url =

Volkovich, Ilya , title =. ECCC , volume = 22, pages = 42, year = 2015, url =

2015
[66]

doi:10.1007/978-3-642-03685-9_52 , note =

Shpilka, Amir and Volkovich, Ilya , title =. doi:10.1007/978-3-642-03685-9_52 , note =

work page doi:10.1007/978-3-642-03685-9_52
[67]

Raghavendra and Sreenivasaiah, Karteek , title =

Mahajan, Meena and Rao, B.V. Raghavendra and Sreenivasaiah, Karteek , title =. doi:10.1007/978-3-319-08783-2_1 , toupdate =

work page doi:10.1007/978-3-319-08783-2_1
[68]

, title =

Roth, Ron M. , title =. , volume = 37, number = 2, pages =
[69]

Proceedings of the Annual ACM Symposium on the Theory of Computing

Nisan, Noam , title =. Proceedings of the Annual ACM Symposium on the Theory of Computing. doi:10.1145/103418.103462 , missing =

work page doi:10.1145/103418.103462
[70]

Saptharishi, Ramprasad , year = 2012, note =

2012
[71]

and Pitassi, Toniann , title =

Grochow, Joshua A. and Pitassi, Toniann , title =. IEEE Annual Symposium on Foundations of Computer Science. doi:10.1109/FOCS.2014.20 , note =

work page doi:10.1109/focs.2014.20 2014
[72]

and Pitassi, Toniann , title =

Joshua A. Grochow and Toniann Pitassi , title =. J. doi:10.1145/3230742 , timestamp =

work page doi:10.1145/3230742
[73]

doi:10.1109/CCC.2011.18 , note =

Anderson, Matthew and van Melkebeek, Dieter and Volkovich, Ilya , title =. doi:10.1109/CCC.2011.18 , note =

work page doi:10.1109/ccc.2011.18 2011
[74]

and Saptharishi, Ramprasad and Shpilka, Amir , title =

Forbes, Michael A. and Saptharishi, Ramprasad and Shpilka, Amir , title =. Proceedings of the Annual ACM Symposium on the Theory of Computing
[75]

Strassen, Volker , title =. J. Reine Angew. Math. , fjournal =
[76]

Foundations and Trends in Theoretical Computer Science , volume = 5, number =

Shpilka, Amir and Yehudayoff, Amir , title =. Foundations and Trends in Theoretical Computer Science , volume = 5, number =
[77]

IEEE Annual Symposium on Foundations of Computer Science

Gupta, Ankit and Kamath, Pritish and Kayal, Neeraj and Saptharishi, Ramprasad , title =. IEEE Annual Symposium on Foundations of Computer Science. doi:10.1109/FOCS.2013.68 , note =

work page doi:10.1109/focs.2013.68 2013
[78]

and Shpilka, Amir and Gupta, Ankit , howpublished =

Forbes, Michal A. and Shpilka, Amir and Gupta, Ankit , howpublished =
[79]

Computational Complexity , VOLUME =

Shpilka, Amir and Wigderson, Avi , title =. Computational Complexity , volume = 10, number = 1, pages =. doi:10.1007/PL00001609 , note =

work page doi:10.1007/pl00001609
[80]

Zippel, Richard , title =

Showing first 80 references.