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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Ajtai, M.: Recursive construction for 3-regular expanders. Combinatorica 14(4), 379–416 (1994)
Alekhnovich, M., Razborov, A.A.: Satisfiability, branch-width and Tseitin tautologies. Computational Complexity 20(4), 649–678 (2011)
Anton, C., Neal, C.: Notes on generating satisfiable SAT instances using random subgraph isomorphism. In: Farzindar, A., Kešelj, V. (eds.) Canadian AI 2010. LNCS, vol. 6085, pp. 315–318. Springer, Heidelberg (2010)
Anton, C.: An improved satisfiable SAT generator based on random subgraph isomorphism. In: Butz, C., Lingras, P. (eds.) Canadian AI 2011. LNCS, vol. 6657, pp. 44–49. Springer, Heidelberg (2011)
Arvind, V., Kurur, P.P., Vijayaraghavan, T.C.: Bounded color multiplicity graph isomorphism is in the #L Hierarchy. In: Proceedings of the 20th Conference on Computational Complexity, pp. 13–27 (2005)
Babai, L.: Monte Carlo algorithms for Graph Isomorphism testing. Tech. Rep. 79-10, Dép. Math. et Stat., Univ. de Montréal (1979)
Beame, P., Culberson, J.C., Mitchell, D.G., Moore, C.: The resolution complexity of random graph k-colorability. Discrete Applied Mathematics 153(1-3), 25–47 (2005)
Beame, P., Impagliazzo, R., Sabharwal, A.: The resolution complexity of independent sets and vertex covers in random graphs. Computational Complexity 16(3), 245–297 (2007)
Beame, P., Pitassi, T.: Simplified and improved resolution lower bounds. In: 37th Annual IEEE Symposium on Foundations of Computer Science, pp. 274–282 (1996)
Ben-Sasson, E., Impagliazzo, R., Wigderson, A.: Near-optimal separation of treelike and general resolution. Combinatorica 24(4), 585–603 (2004)
Ben-Sasson, E., Wigderson, A.: Short proofs are narrow – resolution made simple. Journal of the ACM 48(2), 149–169 (2001)
Cai, J., Fürer, M., Immerman, N.: An optimal lower bound on the number of variables for graph identifications. Combinatorica 12(4), 389–410 (1992)
Chvátal, V., Szemerédi, E.: Many hard examples for resolution. Journal of the ACM 35, 759–768 (1988)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM 5, 394–397 (1962)
Furst, M., Hopcroft, J., Luks, E.: Polynomial time algorithms for permutation groups. In: Proc. 21st IEEE Symp. on Foundations of Computer Science, pp. 36–41 (1980)
Goerdt, A.: The cutting plane proof system with bounded degree of falsity. In: Kleine Büning, H., Jäger, G., Börger, E., Richter, M.M. (eds.) CSL 1991. LNCS, vol. 626, pp. 119–133. Springer, Heidelberg (1992)
Haken, A.: The intractability of resolution. Theoretical Computer Science 39(2-3), 297–308 (1985)
Hirsch, E.A., Kojevnikov, A., Kulikov, A.S., Nikolenko, S.I.: Complexity of semialgebraic proofs with restricted degree of falsity. Journal on Satisfiability, Boolean Modeling and Computation 6, 53–69 (2008)
Immerman, N., Lander, E.: Describing graphs: a first-order approach to graph canonization. In: Selman, A.L. (ed.) Complexity Theory Retrospective, pp. 59–81. Springer (1990)
Jenner, B., Köbler, J., McKenzie, P., Torán, J.: Completeness results for graph isomorphism. J. Comput. Syst. Sci. 66(3), 549–566 (2003)
Köbler, J., Schöning, U., Torán, J.: The Graph Isomorphism problem: Its structural complexity. Birkhauser (1993)
Robinson, J.A.: A machine oriented logic based on the resolution principle. Journal of the ACM 12(1), 23–41 (1965)
Schöning, U., Torán, J.: Das Erfüllbarkeitsproblem SAT - Algorithmen und Analysen, Lehmann (2012)
Torán, J.: On the hardness of Graph Isomorphism. SIAM Journal on Computing 33(5), 1093–1108 (2004)
Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Studies in Constructive Mathematics and Mathematical Logic, Part 2, pp. 115–125. Consultants Bureau (1968)
Urquhart, A.: Hard examples for resolution. Journal of the ACM 34, 209–219 (1987)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Torán, J. (2013). On the Resolution Complexity of Graph Non-isomorphism. In: Järvisalo, M., Van Gelder, A. (eds) Theory and Applications of Satisfiability Testing – SAT 2013. SAT 2013. Lecture Notes in Computer Science, vol 7962. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39071-5_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-39071-5_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39070-8
Online ISBN: 978-3-642-39071-5
eBook Packages: Computer ScienceComputer Science (R0)