A polynomial 3-colorability algorithm with automatic generation of NO 3-colorability (i.e. Co-NP) short proofs

TL;DR

This paper presents a polynomial-time algorithm for planar graph 3-colorability that can generate short, human-readable proofs for non-3-colorable graphs, aiding verification of NO instances despite the problem's NP-completeness.

Contribution

It introduces a polynomial-time algorithm that produces verifiable short proofs for non-3-colorability in planar graphs, bridging NP and Co-NP.

Findings

Algorithm runs in polynomial time

Generates short proofs for NO instances

Exact for non-3-colorable planar graphs

Abstract

In this paper, an algorithm for determining 3-colorability, i.e. the decision problem (YES/NO), in planar graphs is presented. The algorithm, although not exact (it could produce false positives) has two very important features: (i) it has polynomial complexity and (ii) for every "NO" answer, a "short" proof is generated, which is of much interest since 3-colorability is a NP-complete problem and thus its complementary problem is in Co-NP. Hence the algorithm is exact when it determines that a given planar graph is not 3-colorable since this is verifiable via an automatic generation of short formal proofs (also human-readable).