Clique is not solvable by monotone circuits of polynomial size

René Thiemann 🌐

May 8, 2022

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Session Clique_and_Monotone_Circuits