1

私は約 20,000 の制約を作成し、私のマシンではそれらを解決するのに約 3 分かかります。さまざまな種類の制約があり、以下に例を挙げて説明します。アサーションをhttp://filebin.ca/vKcV1gvuGG3にアップロードしました。

より大きな制約システムを解決することに興味があるため、プロセスをスピードアップしたいと考えています。適切な戦術を使用するなどして、それらをより迅速に解決する方法について提案があるかどうかを尋ねたいと思います. 戦略のチュートリアルから、私は戦術を知っていますが、戦術を適用することによってプラスの違いが得られないようです...

liツリーのラベルです。1 番目のタイプは、ラベルの値に制限を加えます。通常、ラベル値は 10 ～ 20 の異なる値の範囲です。

Or(l6 == 11, Or(l6 == 0, l6 == 1, l6 == 2, l6 == 3, l6 == 4,
      l6 == 5, l6 == 6, l6 == 7, l6 == 8, l6 == 9, l6 == 10))

2 番目のタイプは、異なるラベルを相互に関連付けます。

Implies(l12 == 0, Or(l10 == 2, l10 == 5, l10 == 7, l10 == 8, l10 == 10,
           False, False))

3 番目のタイプは、関数f: Int --> Int(f: BitVector --> BitVector完全性を欠く場合は ) を定義して関連付けます。ここで、bound_{s, v}は単なる関数名であり、nはノードの ID です。目標は、関数への満足のいく割り当てを見つけることboundです。

Implies(And(bound_s_v (18) >= 0, l18 == 0),
        And(bound_s_v (19) >= 0,
            bound_s_v (19) >=
            bound_s_v (18),
            bound_s_v (26) >= 0,
            bound_s_v (26) >=
            bound_s_v (18)))

最後のタイプは、境界が必要か ( >= 0)、不要か ( == -1, )を決定します。

Or(bound_s'_v'(0) >= 0, bound_s'_v'(0) == -1)

また、一部の初期状態では境界が必要であるという要件もあります。

`bound_s0_v0(0) >= 0`

実行可能ファイルの説明:最初の 2 ～ 3 行で、スクリプトはソルバーを開始し、z3 をインポートし、最後の行で呼び出しますprint s.check()

4

1 に答える 1

0

おそらく、ロジックに数量詞がないため、ソルバー「qflia」を使用してみてください。

編集：

「qflia」を試してみましたが、速くなりませんでした。おそらく、他のソルバーも試してみてください。

于 2015-08-11T19:58:37.183 に答える