graph - 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

SAT 2013论文“ On the Resolution Complexity of Graph non-Isomorphism ”中描述了Graph Isomorphism问题的SAT编码。

Minisat 是最著名的 SAT 求解器之一，但它有几个可能更快且成功率更高的继任者。试试Cryptominisat（2.9.5 版似乎比 3 版快；它支持并行线程）、Riss3g或Clasp。