Venue
Electron. Colloquium Comput. Complex.
Lower bounds against strong algebraic proof systems and specifically fragments of the Ideal Proof System (IPS), have been obtained in an ongoing line of work.All of these bounds, however, are proved only over large (or characteristic 0) fields, 1 yet finite fields are the more natural setting for propositional proof complexity, especially for progress toward lower bounds for Frege systems such as AC 0 [p]-Frege.This work establishes lower bounds against fragments of IPS over fixed finite fields.Specifically, we show that a variant of the knapsack instance studied by Govindasamy, Hakoniemi, and Tzameret (FOCS'22) has no polynomial-size IPS refutation over finite fields when the refutation is multilinear and written as a constant-depth circuit.The key ingredient of our argument is the recent set-multilinearization result of Forbes (CCC'24), which extends the earlier result of Limaye, Srinivasan, and Tavenas (FOCS'21) to all fields, and an extension of the techniques of Govindasamy, Hakoniemi, and Tzameret to finite fields.We also separate this proof system from the one studied by Govindasamy, Hakoniemi, and Tzameret.In addition, we present new lower bounds for read-once algebraic branching program refutations, roABP-IPS, in finite fields, extending results of Forbes, Shpilka, Tzameret, and Wigderson (Theor. of Comput.'21) and Hakoniemi, Limaye, and Tzameret (STOC'24).Finally, we show that any lower bound against any proof system at least as strong as (nonmultilinear) constant-depth IPS over finite fields for any instance, even a purely algebraic instance (i.e., not a translation of a Boolean formula or CNF), implies a hard CNF formula for the respective IPS fragment, and hence an AC 0 [p]-Frege lower bound by known simulations over finite fields (Grochow and Pitassi (J.ACM'18)).
This paper establishes lower bounds for the Ideal Proof System (IPS) over finite fields, focusing on proof complexity and algebraic lower bounds. The authors demonstrate that IPS has no polynomial-size refutation for the knapsack polynomial mod p, providing a clear obstacle towards achieving superpolynomial lower bounds for AC^0 [p]-Frege. They utilize recent methods, including set-multilinearization, to extend previous results and introduce new lower bounds for read-once algebraic branching program (roABP) refutations. They also present a translation lemma for obtaining CNF proof lower bounds from algebraic instances in finite fields, linking unsatisfiable algebraic expressions to CNF formulations. Additionally, the paper posits a barrier against obtaining non-placeholder lower bounds for roABP-IPS using functional methods, showcasing the limitations within the field of proof complexity in finite fields.
This paper employs the following methods:
- Functional Lower Bound Method
- Lower Bound by Multiples Method
The following datasets were used in this research:
- Super-polynomial lower bounds for constant-depth IPS over finite fields
- New lower bounds for roABP-IPS refutations
- Translation lemma from algebraic instances to CNFs
The authors identified the following limitations:
- It is impossible to establish non-placeholder lower bounds on the size of roABP-IPS refutations when working in finite fields.
- Number of GPUs: None specified
- GPU Type: None specified
- Compute Requirements: None specified