Paper Info
Title
On the resolution complexity of graph non-isomorphism
Abstract
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 graph G into 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 of G. 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.
Year
DOI
Venue
2013
10.1007/978-3-642-39071-5_6
SAT
Keywords
Field
DocType
cfi graph,non-isomorphism formula,resolution refutation,resolution complexity,graph non-isomorphism,resolution width,tree-like resolution refutation,cnf formula,initial formula,polynomial size,color class,graphs pair
Discrete mathematics,Indifference graph,Combinatorics,Graph isomorphism,Partial k-tree,Chordal graph,Cograph,Graph product,Pathwidth,1-planar graph,Mathematics
Conference
Citations 
PageRank 
References 
4
0.41
26
Authors
1
Name
Order
Citations
PageRank
Jacobo Torán156449.26