一种多项式3-可着色算法及NO 3-可着色（即Co-NP）短证明的自动生成
A polynomial 3-colorability algorithm with automatic generation of NO 3-colorability (i.e. Co-NP) short proofs
摘要：
本文给出了平面图3-可染性的判定算法，即判定问题（YES/NO）。该算法虽然不精确（可能产生误报），但有两个非常重要的特征：（i）它具有多项式复杂度;（ii）对于每个“否”答案，都会生成一个“简短”证明，这是非常有趣的，因为3-着色性是NP完全问题，因此其互补问题是Co-NP。因此，该算法是准确的，当它确定一个给定的平面图是不是3-着色，因为这是通过自动生成的简短的正式证明（也是人类可读的）验证。
英文摘要：
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).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
