Clique is not solvable by monotone circuits of polynomial size

 

Title: Clique is not solvable by monotone circuits of polynomial size
Author: René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at)
Submission date: 2022-05-08
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.

BibTeX:
@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},
}
License: BSD License
Depends on: Stirling_Formula, Sunflowers
Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.