我正在使用 Z3 求解器并在 C# 中实现。我在其 .Net API ( http://z3.codeplex.com/SourceControl/latest#examples/dotnet/Program.cs) 的描述中使用了 Microsoft 给出的示例。在这个例子中,我尝试用我自己的模型替换函数“UnsatCoreAndProofExample”中的模型,即:
Expr x = ctx.MkConst("x", ctx.MkIntSort());
Expr y = ctx.MkConst("y", ctx.MkIntSort());
Expr zero = ctx.MkNumeral(0, ctx.MkIntSort());
Expr one = ctx.MkNumeral(1, ctx.MkIntSort());
Expr five = ctx.MkNumeral(5, ctx.MkIntSort());
BoolExpr constraint1 = ctx.MkBoolConst("Constraint1");
solver.AssertAndTrack(ctx.MkGt((ArithExpr)x, (ArithExpr)zero), constraint1);
BoolExpr constraint2 = ctx.MkBoolConst("Constraint2");
solver.AssertAndTrack(ctx.MkEq((ArithExpr)y, ctx.MkAdd((ArithExpr)x, (ArithExpr)one)), constraint2);
BoolExpr constraint3 = ctx.MkBoolConst("Constraint3");
solver.AssertAndTrack(ctx.MkLt((ArithExpr)y, (ArithExpr)five), constraint3);
BoolExpr constraint4 = ctx.MkBoolConst("Constraint4");
solver.AssertAndTrack(ctx.MkLt((ArithExpr)x, (ArithExpr)zero), constraint4);
Status result = solver.Check();
我期望的结果是说在 Unsat 代码中返回了 Constraint1 和 Constraint4。我知道返回 Unsatcore 的设置是正确的,因为当我运行原始的“UnsatCoreAndProofExample”函数时,返回了 unsat Core。但是当我只是将模型更改为上面的模型时,虽然结果是 Unsat 但没有返回 Unsatcore。 所以我的问题是,这可能是因为我编写模型的方式,还是我犯了另一个错误?
最佳答案
基础架构中确实存在一个错误,导致很难正确使用 AssertAndTrack。现在已在不稳定分支中修复(修复为 here )。我还在使用 AssertAndTrack 获取核心的 .NET 和 Java 示例中添加了另一个示例。
关于c# - Z3 和 Unsat 核心案例中的建模约束,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/28558683/