《Information and Computation》：Algorithms for Short Human-Verifiable Proofs of Non-Word-Representability
编辑推荐：
如果一个图能够通过单词中字母的交替出现来表示，则称其为词可表示的（word-representable）。词可表示图类推广了若干重要的图族，并可通过半传递定向（semi-transitive orientations）加以刻画。识别词可表示性是一个NP完全问题
如果一个图能够通过单词中字母的交替出现来表示，则称其为词可表示的（word-representable）。词可表示图类推广了若干重要的图族，并可通过半传递定向（semi-transitive orientations）加以刻画。识别词可表示性是一个NP完全问题，而词可表示图理论中的一个主要瓶颈在于：如何为图的非词可表示性提供高效的证明，而非仅仅依赖于软件验证。
近期，Kitaev和Sun开创了自动生成非词可表示性人类可验证证明的方法，提出了三种算法，并在七个顶点上的25个连通非词可表示图上评估了其性能，而该样本规模相当有限。本文在八个和九个顶点的所有非词可表示图上测试了上述算法，确认了其性能排序。此外，研究人员进一步提出了三种新算法，其中一种在至多九个顶点的图上显著优于此前最佳方法，能够生成明显更短的证明。研究人员将该算法应用于缩短Shrikhande图非词可表示性的已知证明，并为Kneser图K(8, 3)的某个特定子图生成了非词可表示性证明。该子图是文献中已知的首个无三角形（triangle-free）非词可表示图，此前仅以计算证明作为依据。作为研究的副产品，研究人员纠正了反复发表的七个顶点上25个连通非词可表示图列表中的一处错误。
一、研究背景与问题提出
词可表示图理论是图论与词上组合学交叉领域的重要研究方向，其研究价值源于与代数、图论、计算机科学以及调度问题等多领域的深刻联系。词可表示图类推广了若干基础图类，包括圆图（circle graphs）、三色图（3-colorable graphs）和可比图（comparability graphs）等。一个图被称为词可表示的，当且仅当存在一个以顶点集为字母表的单词，使得任意两个不同字母在单词中交替出现当且仅当对应顶点之间有边相连。根据半传递定向定理，一个图是词可表示图当且仅当它允许一个半传递定向，即不存在有向圈和捷径的无环定向。
识别词可表示性已被证明是NP完全问题，这使得证明一个图不是词可表示图成为理论中的核心困难。在以往的研究中，证明非词可表示性主要依赖以下几种途径：构造巧妙的特设论证，但这类论证通常难以构建；穷举所有可能的定向并逐一排除，但这种方法产生的证明规模过于庞大，人类几乎无法验证；穷举所有可能的表示单词，同样面临证明规模爆炸的问题；或者直接引用公开软件的计算结果，但这种方式在学术论证中并不理想。
针对这一瓶颈，Kitaev和Sun在近期工作中开创了自动生成人类可验证的非词可表示性证明的方法，提出了三种算法，并在七个顶点的25个连通非词可表示图上进行了性能评估。然而，这一样本规模相对较小，算法的普适性和性能排序尚需在更大规模的图类上加以验证。
二、研究内容与主要结论
本文的研究工作围绕以下核心问题展开：如何在更大的图类上验证已有算法的性能排序，并进一步开发更高效的证明生成算法。研究人员在八个顶点和九个顶点的所有非词可表示图上系统测试了Kitaev和Sun提出的三种算法，确认了其性能排序的可靠性。在此基础上，研究人员提出了三种新的算法，其中一种在至多九个顶点的图上显著优于此前已知的最佳方法，能够生成明显更短的证明。
该最优算法被应用于两个重要图类的非词可表示性证明：其一，缩短了Shrikhande图的已知非词可表示性证明，将证明长度减少了三分之一；其二，为Kneser图K(8, 3)的某个特定子图生成了非词可表示性证明，该子图是文献中首次报道的无三角形非词可表示图，此前仅以计算证明作为依据。此外，作为研究的副产品，研究人员发现并纠正了反复发表的七个顶点上25个连通非词可表示图列表中的一处错误，其中编号为20的图实际上是可以词表示的，而非此前所认为的非词可表示图。
三、主要技术方法
本文的研究主要依赖以下关键技术方法：基于半传递定向特征的证明搜索算法，利用引理1中关于半传递定向中圈上边定向的结构约束来减少分支搜索空间；分支定界搜索策略，通过逐步定向图中的边并在每一步检查是否产生有向圈或捷径来剪枝；以及基于图同构对称性约简的技术，利用图的对称性减少需要搜索的定向数量。研究人员在实验中未使用定理2中关于源点或汇点假设的简化策略，以保证算法比较的公平性。研究样本包括所有八个顶点和九个顶点的非词可表示图，分别有929个和54957个。
四、研究结果
4.1 算法性能验证与排序确认
研究人员在八个和九个顶点的所有非词可表示图上测试了Kitaev和Sun提出的三种算法，结果表明其在此前七个顶点样本上得到的性能排序在更大规模的图类上仍然成立，验证了该排序的可靠性。
4.2 新算法的提出与性能比较
研究人员提出了三种新的证明生成算法，其中一种在至多九个顶点的图上显著优于此前最佳方法，能够生成明显更短的证明。该算法的核心改进在于更有效地利用引理1中的结构约束，在分支过程中更早地排除不可能产生半传递定向的部分定向。
4.3 Shrikhande图的证明缩短
将最优算法应用于Shrikhande图，该图包含16个顶点和48条边，研究人员成功将其非词可表示性证明的长度减少了三分之一，展示了新算法在实际应用中的优势。
4.4 Kneser图子图的非词可表示性证明
研究人员为Kneser图K(8, 3)的某个特定子图生成了非词可表示性证明，该子图是文献中首次报道的无三角形非词可表示图，此前仅以计算证明作为依据，新算法首次为其提供了人类可验证的证明。
4.5 七顶点非词可表示图列表的修正
研究人员发现此前反复发表的七个顶点上25个连通非词可表示图列表中编号为20的图实际上是词可表示的，并给出了其半传递定向作为证明，纠正了这一长期存在的错误。
五、讨论与结论
本文的研究表明，基于引理1的结构约束可以显著提升非词可表示性证明的自动生成效率，最优算法在至多九个顶点的图上能够生成明显短于此前方法的证明。该算法不仅缩短了Shrikhande图的已知证明，还为无三角形的Kneser图子图提供了首个非计算的人类可验证证明，拓展了能够以人类可验证方式证明非词可表示性的图类范围。研究同时纠正了文献中长期存在的七顶点非词可表示图列表错误，为后续研究提供了更准确的基础数据。
