3

私はZ3を使用して、有界モデルチェッカーを構築しています。完全性テストを実装しようとすると、奇妙なパフォーマンスの問題が発生します。完全性テストでは、すべてのパスに各状態が最大で1回含まれていることをすべての状態で確認する必要があります。この特性を満たすパスがまだある場合、Z3はすぐに答えを出しますが、すべてのパスを考慮した場合、Z3は指数関数的に遅いように見えます。

テストケースを次のように減らしました。

; Set the problem size (length of path)
(define-fun sz () Int 5)

; Used to define valid states
(define-fun limit ((s Int)) Bool
  (and (>= s 0)
       (<= s sz)))

; Constructs a path of a given length
(define-fun path-of-len ((path (Array Int Int)) (len Int)) Bool
  (forall ((i Int))
          (=> (and (>= i 0)
                   (< i len))
          (limit (select path i)))))

; Asserts that a given path only contains unique states
(define-fun loop-free ((path (Array Int Int)) (len Int)) Bool
  (forall ((i Int) (j Int))
          (=> (and (>= i 0)
                   (>= j 0)
                   (< i len)
                   (< j len)
                   (not (= i j)))
              (not (= (select path i) (select path j))))))

; Construct a unique path of a given length
(define-fun path ((path (Array Int Int)) (len Int)) Bool
  (and (path-of-len path len)
       (loop-free path len)))

; Declare a concrete path
(declare-const tpath (Array Int Int))

; Assert that the path is loop free
(assert (path tpath (+ sz 2)))

(check-sat)

私のコンピューターでは、これにより次の実行時間が発生します（パスの長さによって異なります）。

  • 3：0.057秒
  • 4：0.561秒
  • 5：42.602秒
  • 6：> 15m（中止）

Intからサイズ64のビットベクトルに切り替えると、パフォーマンスは少し向上しますが、それでも指数関数的に見えます。

  • 3：0.035秒
  • 4：0.053秒
  • 5：0.061秒
  • 6：0.106秒
  • 7：0.467秒
  • 8：1.809s
  • 9：2分49.074秒

不思議なことに、長さが10の場合、2m34.197秒しかかかりません。小さいサイズのビットベクトルに切り替えると、パフォーマンスは少し向上しますが、それでも指数関数的です。

だから私の質問は：これは予想されることですか？この「ループのない」制約を定式化するためのより良い方法はありますか？

4

2 に答える 2

1

あなたの公式は本質的に「ピジョンホール」問題をエンコードしています。sz+1穴（値0、1、…、sz）とsz+2鳩（配列セル(select tpath 0)、…、 ）があります(select tpath (+ sz 1))。最初の数量詞は、各鳩を穴の1つに入れる必要があると述べています。2つ目は、2つの異なるハトが同じ穴に入らないようにすることです。

「ピジョンホール」問題の多項式サイズ分解能の証明はありません。したがって、実行時間の指数関数的成長が期待されます。解像度、DPLL、またはCDCLに基づくSATソルバーは、鳩の穴の問題に対してうまく機能しないことに注意してください。

Z3はビットベクトルを命題論理に還元し、ケース分析はそのレベルではるかに効率的であるため、ビットベクトルを使用するとパフォーマンスが向上します。

ところで、パラメトリック問題をエンコードするために数量詞を使用しています。これは洗練されたソリューションですが、Z3にとって最も効率的なアプローチではありません。Z3の場合、一般に、「拡張された」数量詞のない問題を主張する方が適切です。ただし、質問で説明されている問題については、指数関数的成長が続くため、大きな違いはありません。

于 2011-10-27T16:52:46.097 に答える
0

レオナルドが言ったように、鳩の穴の問題は本質的に指数関数的であるため、最終的にはパフォーマンスが低下します。おそらくあなたができる唯一のことは、パフォーマンスが悪くなる時間を延期することです。あなたはビットベクトルを試したので、私の提案は、問題のサイズが事前に定義されていることを前提として、Leonardoによって提案されたように、問題を数量詞のない問題に変換してみて、いくつかの戦術を使用してみてください。

于 2015-08-12T04:29:55.620 に答える