Near-optimal lower bounds for depth-n parity decision DAGs

The Strong Exponential Time Hypothesis (SETH) conjectures that deciding satisfiability of Boolean formulas requires essentially 2^n computational steps in the worst case, where n is the number of variables. Recently, OpenAI announced that an internal AI model had found a disproof of this hypothesis, a claim still awaiting independent verification. Nevertheless, such lower bounds can still be established unconditionally for restricted computational models.

In this talk, we establish such a lower bound for parity decision DAGs (directed acyclic graphs), a generalization of the decision DAG representation of the resolution proof system. Given an assignment to an unsatisfiable CNF formula, such a DAG must find a clause falsified by the assignment, using queries of linear functions over F_2.

More precisely, for every \epsilon > 0, we construct unsatisfiable CNF formulas on n variables such that every parity decision DAG of depth at most n has size at least 2^((1−\epsilon)n). This lower bound is essentially optimal, matching the complexity of exhaustive search up to an arbitrarily small loss in the exponent.

I will explain the main ideas behind the proof, including random walks on decision DAGs and a lifting argument using randomly chosen Boolean gadgets.

No prior knowledge of computational complexity or proof complexity is required.

Joint work with Klim Efremenko (STOC 2026).