Constant-Depth Frege Systems with Counting Axioms Polynomially Simulate Nullstellensatz Refutations

TL;DR

This paper demonstrates that constant-depth Frege systems with counting axioms can efficiently simulate Nullstellensatz refutations modulo m, leading to new insights and size separations in proof complexity.

Contribution

It introduces a new reducibility concept from formulas to polynomial systems and establishes the first size separation between Nullstellensatz and polynomial calculus refutations.

Findings

Constant-depth Frege systems with counting axioms simulate Nullstellensatz refutations.

Established the first size separation between Nullstellensatz and polynomial calculus.

Provided new small refutations for certain CNFs.

Abstract

We show that constant-depth Frege systems with counting axioms modulo $m$ polynomially simulate Nullstellensatz refutations modulo $m$. Central to this is a new definition of reducibility from formulas to systems of polynomials with the property that, for most previously studied translations of formulas to systems of polynomials, a formula reduces to its translation. When combined with a previous result of the authors, this establishes the first size separation between Nullstellensatz and polynomial calculus refutations. We also obtain new, small refutations for certain CNFs by constant-depth Frege systems with counting axioms.