Email Gateway (May 08 2022 at 12:30): Email Gateway (May 08 2022 at 12:30):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
I'm happy to announce a new AFP entry:
Clique is not solvable by monotone circuits of polynomial size by René Thiemann.
Given a graph G with n vertices and a number s, the decision problem Clique asks whether
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.
https://www.isa-afp.org/entries/Clique_and_Monotone_Circuits.html
Enjoy,
Andreas
Last updated: Jan 04 2025 at 20:18 UTC