我使用 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]
正如预期的那样。但是,当我尝试通过将找到的分配和否定并将其添加回 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 任务。IE:
[true; true; z]
为什么之前true
更改为z 的分配z
?