ABSTRACT. Given a family of CNF formulas F, the size-width inequality in Resolution reduces the hard problem of proving strong (say exponential) lower bounds on the number of clauses needed to refute F in resolution to the easier problem of proving strong enough (say linear) lower bounds on the width of the clauses needed to refute F in resolution. Similar results connect the degree and size in the proof systems Polynomial Calculus, Sherali-Adams, Sum-of-Squares and Positivstellensatz. In this talk we present a simplified argument for the result on Sherali-Adams, Sum-of-Squares, in the special case when all input polynomials are monomials (or Boolean axioms).

ABSTRACT. 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 whereas finite fields form the more natural setting for propositional proof complexity. This work establishes lower bounds against fragments of IPS over constant-sized finite fields, resolving an open problem left by a series of prior works beginning with Forbes, Shpilka, Tzameret, and Wigderson (Theor. of Comput.’21), persisting with Behera, Limaye, Ramanathan, and Srinivasan (ICALP’25), and most recently posed by Forbes (CCC’24). We further highlight the importance of the constant-sized finite field regime in IPS by showing that any hard instance in this regime for a sufficiently strong proof system translates into a hard instance against AC0[p]-Frege, whose lower bounds remain a longstanding open problem. In particular, we show the following. Constant-depth multilinear IPS: We prove 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. Our argument has two key ingredients: (i) the recent set-multilinearization result of Forbes, which extends the earlier result of Limaye, Srinivasan, and Tavenas (J. ACM’25) to all fields; and (ii) an extension of the techniques of Govindasamy et al. to finite fields, obtained by constructing a new knapsack variant and generalizing the degree lower bound used in their work. This improves on Behera et al. who obtained related results for fragments of IPS over fields of positive characteristic. Their result requires the field size to grow with the instance, whereas ours does not. Hence, in the constant positive characteristic setting, our IPS lower bound subsumes theirs as it also holds over constant-sized finite fields. Moreover, we separate our proof system from that of Govindasamy et al. by constructing a further knapsack variant and proving a new degree lower bound. Read-once ABP IPS: We present new lower bounds for read-once algebraic branching pro- gram refutations, roABP-IPS, in finite fields, extending results of Forbes et al. and Hakoniemi, Limaye, and Tzameret (STOC’24). Algebraic-to-CNF translation: We show that any lower bound against any proof system at least as strong as (non-multilinear) 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 AC0[p]-Frege lower bound by known simulations over finite fields (Grochow and Pitassi (J. ACM’18)).

ABSTRACT. We consider the Ideal Proof System (IPS) introduced by Grochow and Pitassi and pose the question of which tautologies admit symmetric proofs, and of what complexity. The symmetry requirement in proofs is inspired by recent work establishing lower bounds in other symmetric models of computation. We link the existence of symmetric IPS proofs to the expressive power of logics such as fixed-point logic with counting and choiceless polynomial time, specifically regarding the graph isomorphism problem. We identify relationships and tradeoffs between the symmetry of proofs and other parameters of IPS proofs such as size, degree and depth. We study these on a number of standard families of tautologies from proof complexity and finite model theory such as the pigeonhole principle, the subset sum problem and the Cai-Fürer-Immerman graphs, exhibiting non-trivial upper bounds on the size of symmetric IPS proofs.

ABSTRACT. Cardinality constraints are one of the most widely used high-level constraints in SAT-based reasoning. Recently, it has been observed experimentally that the input ordering of cardinality encodings can significantly affect the performance of SAT solvers, sometimes even more than the choice of the encoding itself. In this paper, we study this phenomenon from a proof-complexity perspective, showing that encoding the contradictory pair of constraints $x_1+\cdots+x_n \geq k+1$ and $x_1+\cdots+x_n \leq k$, with totalizers and different input orderings, gives rise to exponentially hard formulas for Resolution.

ABSTRACT. In this work we examine the strength of various cutting planes-like proof systems, where we replace the division rule with other inference rules, such as the saturation rule or a (lifted) cover cut rule, which include rules that can derive implied clauses or implied cardinalities and the rounding and index cover cuts. In particular, we show implicational separations between increasingly strong lifted cover cuts, and between cover cuts and saturation. We also show that the index cover cut can be simulated using the rounding cover cut, but that any such simulation requires a linear number of steps.

ABSTRACT. We compare the complexity of a range of new cutting planes (CP) subsystems that exploit cardinality constraints. We show CP paired with cuts from linear programming and mixed integer programming can be powerful especially when considering such cardinality constraints. Through this investigation we re-examine the power of saturation and find an exponential refutation separation between it and these new subsystems.