0

Z3 を単純な SAT ソルバーとして使用し、次のように命題を主張しています。

let ctx = new Context()
let x = ctx.MkBoolConst("x")
let y = ctx.MkBoolConst("y")
let z = ctx.MkBoolConst("z")
let f = ctx.MkOr(ctx.MkAnd(x,y), ctx.MkAnd(ctx.MkNot(x),z))
let s = ctx.MkSolver()
s.Assert(f)
assert (s.Check() = Status.SATISFIABLE)
let r= [s.Model.Eval(x); s.Model.Eval(y); s.Model.Eval(z)]
printfn "%A" r

どちらが返されますか

[false; true; true]

予想通り。ただし、見つかった割り当ての and を取り、それを否定して Z3 ソルバーに追加し直すことで、Z3 にさらなる解決策を求めようとすると、

let mkB(z3_lit:BoolExpr,bvalue:Expr) = 
  if (bvalue:?> BoolExpr).IsTrue then z3_lit else ctx.MkNot z3_lit
let founds = List.map mkB (List.zip [x;y;z] r)
let and_founds = ctx.MkAnd (List.toArray(founds))
let negated = ctx.MkNot and_founds
s.Assert negated
assert (s.Check() = Status.SATISFIABLE)
let r2 = [s.Model.Eval(x); s.Model.Eval(y); s.Model.Eval(z)]
printfn "%A" r2

z への奇妙な割り当てを取得します。すなわち:

[true; true; z]

true以前に変更された z への代入はなぜzですか?

4

1 に答える 1

1

私が間違っていなければ、変数を独自のモデルとして取得することは、それが「ドント ケア」であることを意味します。どの値でもz有効なモデルが得られます。実際、この場合、節はすでに満たされx、y真です。

Z3 にモデルを完成させたい場合は、この質問をご覧ください。

また、C API は、少なくとも への追加の引数を定義しZ3_model_evalます。これを使用して、すべての変数の値が必要であることを Z3 に示すことができます。

于 2013-03-24T11:09:03.350 に答える