### Abstract

Given a graph $G$ with $n$ vertices and a number $s$, the decision problem Clique asks whether $G$ contains a fully connected subgraph with $s$ vertices. For this NP-complete problem there exists a non-trivial lower bound: no monotone circuit of a size that is polynomial in $n$ can solve Clique.

This entry provides an Isabelle/HOL formalization of a concrete lower bound (the bound is $\sqrt[7]{n}^{\sqrt[8]{n}}$ for the fixed choice of $s = \sqrt[4]{n}$), following a proof by Gordeev.

### License

BSD License

### Topics

- Mathematics/Combinatorics

### Session Clique_and_Monotone_Circuits

- Preliminaries
- Monotone_Formula
- Assumptions_and_Approximations
- Clique_Large_Monotone_Circuits

### Depends on

- Stirling’s formula
- The Sunflower Lemma of Erdős and Rado

### Auto-related entries

- Extensions to the Comprehensive Framework for Saturation Theorem Proving
- Formalization of Concurrent Revisions
- Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals
- The Divergence of the Prime Harmonic Series

## Cite

×

Clique_and_Monotone_Circuits-AFP

    @article{Clique_and_Monotone_Circuits-AFP,
      author  = {René Thiemann},
      title   = {Clique is not solvable by monotone circuits of polynomial size},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Clique_and_Monotone_Circuits.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- May 8, 2022 : Isabelle2021-1