子圖同構到SAT

Question

的子圖同構（SI）的問題是其中兩個圖G和H作爲輸入給出的計算任務，並必須確定G是否包含一個子圖是同構的H.

這是一個NP-Complete問題。

我想知道它與SAT問題的關係。
特別是，我希望這個問題的實例可以在整個SAT求解程序中解決（如miniSAT）。我需要一個算子，它可以在多項式時間內從SI映射到SAT問題，然後可以使用SAT分配來查找映射從G的節點到H的節點。

任何想法???

Answer 1

甲SAT編碼爲圖同構問題在SAT 2013紙「On the Resolution Complexity of Graph non-Isomorphism」中所述。

Minisat是最着名的SAT求解器之一，但它有幾個後繼可能更快，成功率更高。嘗試Cryptominisat（版本2.9.5似乎比版本3快;它支持並行線程），Riss3g或Clasp。