On the Resolution Complexity of Graph Non-isomorphism
On the Resolution Complexity of Graph Non-isomorphism
复制标题
关于图非同构的解析复杂度
DOI：
10.1007/978-3-642-39071-5_6
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Jacobo Torán
中科院分区：
文献类型：
--
作者：
Jacobo Torán
对于一对给定的图，我们将同构原理以自然的方式编码为顶点数为多项式大小的CNF公式，当且仅当图是同构的。使用[12]中的CFI图，我们可以将任意无向图转换为一对非同构图。我们证明了图同构公式的任何反驳的分辨宽度都有一个与g的展开性质有关的下界。利用这一事实，我们提供了一个非同构图对的显式族，对于这些非同构图对，任何解析反驳都需要初始公式大小中的指数子句数。这些图对用以4为界的颜色多重性着色。相反，我们表明，当颜色类被限制为大小为3或更小时，非同构公式具有多项式大小的树状分辨率反驳。
For a pair of given graphs we encode the isomorphism principle in the natural way as a CNF formula of polynomial size in the number of vertices, which is satisfiable if and only if the graphs are isomorphic. Using the CFI graphs from [12], we can transform any undirected graphGinto a pair of non-isomorphic graphs. We prove that the resolution width of any refutation of the formula stating that these graphs are isomorphic has a lower bound related to the expansion properties ofG. Using this fact, we provide an explicit family of non-isomorphic graph pairs for which any resolution refutation requires an exponential number of clauses in the size of the initial formula. These graphs pairs are colored with color multiplicity bounded by 4. In contrast we show that when the color classes are restricted to have size 3 or less, the non-isomorphism formulas have tree-like resolution refutations of polynomial size.
登录
查看更多内容
Das Erfüllbarkeitsproblem SAT - 算法与分析
DOI：
--
发表时间：
2012
期刊：
Mathematik für Anwendungen
影响因子：
--
作者：
Uwe Schöning;J. Torán
通讯作者：
J. Torán
DOI：
--
发表时间：
1990
期刊：
影响因子：
--
作者：
N. Immerman;E. Lander
通讯作者：
E. Lander
基于随机子图同构的改进可满足SAT生成器
DOI：
--
发表时间：
2011
期刊：
Canadian Conference on AI
影响因子：
--
作者：
Calin Anton
通讯作者：
Calin Anton
使用随机子图同构生成可满足的 SAT 实例
DOI：
--
发表时间：
2009
期刊：
Canadian Conference on AI
影响因子：
--
作者：
Calin Anton;L. Olson
通讯作者：
L. Olson
随机图k-着色性的分辨率复杂度
影响因子：
1.1
作者：
P. Beame;J. Culberson;D. Mitchell;Cristopher Moore
通讯作者：
Cristopher Moore