Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Supercritical Tradeoffs for Monotone Circuits

Mika Göös, Gilbert Maystre, Kilian Risse, Dmitry Sokolov

TL;DR

A new family of unsatisfiable 3-CNF formulas (called bracket formulas) are introduced that admit resolution refutations of quasipolynomial size while any refutation of polynomial depth requires exponential size.

Abstract

We exhibit a monotone function computable by a monotone circuit of quasipolynomial size such that any monotone circuit of polynomial depth requires exponential size. This is the first size-depth tradeoff result for monotone circuits in the so-called supercritical regime. Our proof is based on an analogous result in proof complexity: We introduce a new family of unsatisfiable 3-CNF formulas (called bracket formulas) that admit resolution refutations of quasipolynomial size while any refutation of polynomial depth requires exponential size.

Supercritical Tradeoffs for Monotone Circuits

TL;DR

A new family of unsatisfiable 3-CNF formulas (called bracket formulas) are introduced that admit resolution refutations of quasipolynomial size while any refutation of polynomial depth requires exponential size.

Abstract

We exhibit a monotone function computable by a monotone circuit of quasipolynomial size such that any monotone circuit of polynomial depth requires exponential size. This is the first size-depth tradeoff result for monotone circuits in the so-called supercritical regime. Our proof is based on an analogous result in proof complexity: We introduce a new family of unsatisfiable 3-CNF formulas (called bracket formulas) that admit resolution refutations of quasipolynomial size while any refutation of polynomial depth requires exponential size.

Paper Structure

This paper contains 24 sections, 21 theorems, 21 equations, 3 algorithms.

Table of Contents

  1. Introduction
  2. New technique: Bracket formulas
  3. CNF encoding with pointers.
  4. Proof overview.
  5. Genealogy of bracket formulas.
  6. Related work: Monotone circuit complexity
  7. Related work: Proof complexity
  8. Hardness condensation.
  9. Concurrent work by dRF25
  10. Bracket Formulas
  11. Large-alphabet encoding
  12. CNF encodings
  13. Wide formula.
  14. Narrow formula.
  15. Upper Bound
  16. ...and 9 more sections

Key Result

Theorem 1

There is a monotone $f\colon \{0, 1\}^n \to \{0, 1\}$ such that:

Theorems & Definitions (39)

  • Theorem 1: Main result for circuits
  • Theorem 2: Main result for proofs
  • Theorem 3
  • Theorem 4
  • Proposition 4
  • Proposition 4
  • Theorem 4
  • Theorem 4
  • Definition 5: Configuration
  • Definition 6: Domination
  • ...and 29 more