1

これを達成する方法についての提案を期待しています:

定義: 無向グラフ G は、頂点の集合 V と辺の集合 E によって定義されます。ここで、各辺はサイズ 2 の V のサブセット、つまり頂点の順序付けられていないペア {u, v} です。G の長さ k のサイクルは、{v_1, v_2}, {v_2, v_3}, ..., {v_k-1, v_k}, {v_k, v_1 の異なる頂点のシーケンス v_1, ..., v_k です。 G のハミルトニアン サイクルは、長さ n = |V| のサイクル、つまり、グラフの各頂点を 1 回だけ通過する chcle です。ハミルトニアン サイクルを持つ場合、G ハミルトニアンと呼びます。

問題: 次の決定問題の命題論理定式化を提供します: 無向グラフ G が与えられた場合、G はハミルトニアンですか? 製剤は Z3 によってチェックされます。

入力形式は次のとおりです。

4
0 1
1 2
2 3
3 0
1 3

ここで、最初の数字は頂点の数を表し、残りのペアはすべて G のエッジです。

出力は次のようになります: 0 1 2 3

明らかに、出力は常に数値 1、...、n-1 の順列になります。ここで、n = |V| です。しかし、命題論理のみを使用して整数を操作する方法がわかりません。

アドバイスをいただければ幸いです。

よろしく。

これは、指定された入力に対して機能するソリューションです。エッジの組み合わせ (n Choose k) を生成する perl ルーチンを書くことができれば、これを任意の数の入力に一般化できます。

(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)

(declare-const e1 Bool)
(declare-const e2 Bool)
(declare-const e3 Bool)
(declare-const e4 Bool)
(declare-const e5 Bool)

(assert (xor (and e1 e2 e3 e4) (and e1 e2 e3 e5) (and e1 e2 e4 e5) (and e1 e3 e4 e5) (and e2 e3 e4 e5)))

(assert (and v0 v1 v2 v3))

(assert (=> e1 (and v0 v1)))
(assert (=> e2 (and v1 v2)))
(assert (=> e3 (and v2 v3)))
(assert (=> e4 (and v3 v0)))
(assert (=> e5 (and v1 v3)))

(check-sat)
(get-model)
4

2 に答える 2

2

アイデアは、SMT ソルバーに n 個の数値 (a1..an など) を生成させ、次のすべてをアサートすることです。

  • これらの数値はすべて 0 から n-1 の間です
  • すべての数値が異なります
  • 頂点 a1 .. an はサイクルを形成します。つまり、a1-a2、a2-a3、...、a(n-1)-an および an-a1 の間にエッジがあることを確認します。

つまり、「ハミルトニアン サイクル」とは何かを説明するだけで、存在する場合は SMT ソルバーが検出します。

ここで問題となるのは、これらすべてを SMTLib2 で表現して、Z3 が解析できるようにする方法です。確かにそれは可能ですが、SMT ソルバーへのバインディングを提供する高水準言語を使用することをお勧めします。Haskell と Scala は、たとえば Z3 をスクリプト化できる 2 つの言語です。そうすれば、問題に集中するだけで、ホスト言語が舞台裏で翻訳を処理します。これには、ホスト言語と関連するライブラリを学習するための投資が必要ですが、私の意見では、それだけの価値があります。

たとえば、Haskell と Z3 を使用してこの問題を解決する方法は次のとおりです: http://gist.github.com/1715097。ソリューションは、Haskell のわずか 7 行であり、それを使用して、任意のサイズのグラフをクエリできます。このソリューションは、Haskell の表現力と Z3 の SMT ソルバー機能を利用して、クリーンなインターフェイスを提供します。

于 2012-02-01T04:32:50.353 に答える