Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Clique is not solvable by mono...


view this post on Zulip 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: Jul 15 2022 at 23:21 UTC