graph - SAT へのサブグラフ同型

Question

Subgraph Isomorphism (SI) 問題は、2 つのグラフ G と H が入力として与えられる計算タスクであり、G に H と同型のサブグラフが含まれているかどうかを判断する必要があります。

これはNP 完全問題です。

SAT問題との関係を知りたいです。特に、この問題のインスタンスを SAT ソルバー ( miniSAT
など) 全体で解決できるようにしたいと考えています。SI から SAT 問題へのマッピングを多項式時間で実行できるアルゴリズムが必要であり、SAT 割り当てを使用してノードからマッピングを見つけることができます。 G から H のノードへ。

何か案が ？？？

Answer 1

Graph Isomorphism問題のSATエンコーディングについては、 SAT 2013の論文「On the Resolution Complexity of Graph non-Isomorphism」で説明されています。

Minisat は最もよく知られている SAT ソルバーの 1 つですが、おそらくより高速で成功率の高い後継モデルがいくつかあります。Cryptominisat (バージョン 2.9.5 はバージョン 3 より高速のようです。並列スレッドをサポートしています)、Riss3gまたはClaspを試してください。