0

これは主に論理的な問題だと思います...

私はこの smtlib 式を使用します:

(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(declare-fun d () Bool)
(assert (xor (and a (xor b c)) d))

この構造の用語はどれですか（少なくとも私の意見では）：

    XOR
    | |
  AND d
  | |
  a XOR
    | |
    b c

私の推測: resultSet は次のようになります。

{ab, ac, d}

しかし、これはscala^z3 ctx.checkAndGetAllModels()を使用しています:

{ab, d, ac, ad, abcd}

ad と abcd が入っているのはなぜですか? 期待した結果だけを得ることができますか?

4

1 に答える 1

3

Scala (Z3 なし) を使用して、実際には制約に対する解決策が他にもあることを示します。

val tf = Seq(true, false)
val allValid =
  for(a <- tf; b <- tf; c <- tf; d <- tf; 
      if((a && (b ^ c)) ^ d)) yield (
    (if(a) "a" else "") + (if(b) "b" else "") +
    (if(c) "c" else "") + (if(d) "d" else ""))

allValid.mkString("{ ", ", ", " }")

版画:

{ abcd, ab, ac, ad, bcd, bd, cd, d }

だから私が何かを見逃していない限り、問題は、なぜすべての解決策を見つけられないのですか? これがその答えです。(ネタバレ注意: 「getAllModels」は実際にはすべてのモデルを取得するわけではありません。) まず、観察したことを再現しましょう。

import z3.scala._
val ctx = new Z3Context("MODEL" -> true)
val a = ctx.mkFreshConst("a", ctx.mkBoolSort)
val b = ctx.mkFreshConst("b", ctx.mkBoolSort)
val c = ctx.mkFreshConst("c", ctx.mkBoolSort)
val d = ctx.mkFreshConst("d", ctx.mkBoolSort)
val cstr0 = ctx.mkXor(b, c)
val cstr1 = ctx.mkAnd(a, cstr0)
val cstr2 = ctx.mkXor(cstr1, d)
ctx.assertCnstr(cstr2)

ここで、: を実行するとctx.checkAndGetAllModels.foreach(println(_))、次のようになります。

d!3 -> false
a!0 -> true
c!2 -> false
b!1 -> true

d!3 -> true    // this model is problematic
a!0 -> false

d!3 -> false
a!0 -> true
c!2 -> true
b!1 -> false

d!3 -> true
a!0 -> true
c!2 -> false
b!1 -> false

d!3 -> true
a!0 -> true
c!2 -> true
b!1 -> true

ここでの問題は、2 番目のモデルが不完全なモデルであることです。Z3 はそれを返すことができます。これは、bとの値が何であれc、制約が満たされるためです (bとcはドントケア変数です)。の現在の実装ではcheckAndGetAllModels、繰り返しを防ぐためにモデルを否定するだけです。この場合、(not (and d (not a)))成立するような別のモデルを要求します。これにより、この 2 つの値を持つ他のすべてのモデルが返されなくなります。ある意味では、不完全なモデルは実際には 4 つの有効で完成したモデルを表しています。

ちなみに、このfindAll関数で ScalaZ3 の DSL を使用するとどうなるかというと、すべてのモデルが不完全な場合 (および次のモデルの計算に使用される前) にデフォルト値で完成されます。DSL のコンテキストでは、式に現れる一連の変数を知っているので、これを行うことができます。この場合、モデルをどのように完成させるべきかを推測するのは難しくなります。1 つのオプションは、使用された変数を ScalaZ3 が記憶できるようにすることです。より良い解決策は、Z3 が常に don't-care 変数の値を返すか、単にモデル内のすべてのdon't-care変数をリストするオプションを持つことです。

于 2011-12-09T18:51:38.367 に答える