Another look at graph coloring via propositional satisfiability
Another look at graph coloring via propositional satisfiability
复制标题
DOI：
10.1016/j.dam.2006.07.016
复制
发表时间：
2008-01-15
影响因子：
1.1
通讯作者：
Van Gelder, Allen
中科院分区：
文献类型：
--
作者：
Van Gelder, Allen
本文研究了图着色问题的求解方法，将其转化为命题可满足性问题。该研究涵盖了三种基于后序推理的可满足性求解器（例如，掌握，干扰），前序推理（例如，2cl、2clsEq）和后链（莫多克）。该研究评估了三种编码，其中一种被认为是新的。针对着色问题，采用了一些新的破界方法来减少解的冗余。这项研究的一个副产品是一种实现的下界技术，该技术已经显示出长期未解决的随机图（称为DSJC 125.5和DSJC 125.9）的色数的下界得到了改进。独立集分析表明，DSJC 125.5和DSJC 125.9的色数分别至少为18和40，但可满足性编码只能证明在可用的时间和空间内，色数分别至少为13和38。(C)2007 Elsevier B.V.保留所有权利。
This paper studies the solution of graph coloring problems by encoding into propositional satisfiability problems. The study covers three kinds of satisfiability solvers, based on postorder reasoning (e.g., grasp, chaff), preorder reasoning (e.g., 2cl, 2clsEq), and back-chaining (modoc). The study evaluates three encodings, one of them believed to be new. Some new symmetry-breaking methods, specific to coloring, are used to reduce the redundancy of solutions. A by-product of this research is an implemented lower-bound technique that has shown improved lower bounds for the chromatic numbers of the long-standing unsolved random graphs known as DSJC125.5 and DSJC125.9. Independent-set analysis shows that the chromatic numbers of DSJC125.5 and DSJC125.9 are at least 18 and 40, respectively, but satisfiability encoding was able to demonstrate only that the chromatic numbers are at least 13 and 38, respectively, within available time and space. (C) 2007 Elsevier B.V. All rights reserved.