Subgraph isomorphism to SAT

Question

The Subgraph Isomorphism (SI) problem is a computational task in which two graphs G and H are given as input, and one must determine whether G contains a subgraph that is isomorphic to H.

This is a NP-Complete problem .

I want to know its relation with the SAT problem.
In particular, I want instances of this problem can be solved throughout SAT Solver(like miniSAT).I need an alorithm which can do a mapping from SI to SAT problem in polynomial time and then SAT assignment can be used to find a mapping from nodes of G to nodes of H .

Any idea ???

Answer 1

A SAT encoding for the Graph Isomorphism problem is described in the SAT 2013 paper "On the Resolution Complexity of Graph non-Isomorphism".

Minisat is one of the best-known SAT solvers, but it has several successors which are probably faster and have a higher success rate. Try Cryptominisat (version 2.9.5 seems to be faster than version 3; it supports parallel threads), Riss3g or Clasp.