Z3：使用 Java API 简化断言

Question

我在 Windows 7 和 Java 7 64 位上使用 Z3 版本 4.3.2 64 位的 Java-API。

我正在尝试使用简化来了解我的断言集中的冗余信息。

我的第一个尝试是简化布尔表达式并像这样评估结果

Expr e = ctx.mkImplies(ctx.mkBoolConst("A"),ctx.mkBoolConst("B")).simplify();

在我的例子中

(=> A B)            
(=> (not B) C)
(=> A B)
(=> B A)
(=> D E)
(=> B F)
(=> G D)
(=> H I)
(=> I (not D))
(=> (not D) I)
(=> C (not B))
C)

这会产生一个简化的公式

(and 
    (or (not A) B)
    or B C)
    or (not B) A)
    (or (not D) E)
    (or (not B) F)
    (or (not G) D)
    (or (not H) I)
    (or (not I) (not D))
    (or D I)
    (or (not C) (not B))
    C
)

我之前将含义包装在一个 AND 表达式中，以便将它们简化为一个表达式。

这个结果还不是我想要的。去掉了原代码第三行的重复规则（没问题）。 但如果 C 为真（示例的最后一行），则 B 必须为假 ((=> C (not B)))。 如果 B 为假，则 A 必须为假 ((=> A B))。 等等……

我的expexted更像是下面的（我是手动做的，所以转换可能有错误）

(and 
    (or (not A) B)       ; transformed to (not A)
    or B C)              ; transformed to C
    or (not B) A)        ; deleted
    (or (not D) E)       ; left unchanged
    (or (not B) F)       ; deleted
    (or (not G) D)       ; left unchanged
    (or (not H) I)       ; left unchanged
    (or (not I) (not D)) ; left unchanged
    (or D I)             ; left unchanged
    (or (not C) (not B)) ; transformed to (not B)
    C                    ; C
)

接下来，我尝试使用如下策略

Tactic simplifyTactic = ctx.mkTactic("ctx-solver-simplify");
Tactic smtTactic = ctx.mkTactic("smt");
Tactic then = ctx.then(simplifyTactic, smtTactic, new Tactic[] {});
Solver solver = ctx.mkSolver(then);
solver.add(bel2.toArray(new BoolExpr[0])); // bel2 is List<BoolExpr>
Status status = solver.check();

这样做会导致模型而不是简化。 此外，对我来说，让简化策略完全奏效有点困难。 结果通常是 UNKNOWN，原因是“不完整”。

我上面描述的预期结果完全可以用 Z3 计算吗？怎么办？

我已经在这个论坛上四处看了看，但我的观点并没有得到真正的回答......

Answer 1

作为一种策略，smt 不会导致您尝试实现的断言的任何转换或简化，这是可满足性策略，因此对于某些断言，它将返回 sat、unsat、unknown、或者可能会超时。

使用简化策略更符合您的需求，但您可能需要应用不同的策略来实现所需的转换。但是，当我将您的问题编码为 SMT-LIB 格式并在您尝试时使用 ctx-solver-simplify 策略时，它返回了我认为您正在寻找的内容（rise4fun 链接：http://rise4fun.com/Z3/r2id）：

(declare-fun A () Bool)
(declare-fun B () Bool)
(declare-fun C () Bool)
(declare-fun D () Bool)
(declare-fun E () Bool)
(declare-fun F () Bool)
(declare-fun G () Bool)
(declare-fun H () Bool)
(declare-fun I () Bool)

(assert (and (=> A B)            
(=> (not B) C)
(=> A B)
(=> B A)
(=> D E)
(=> B F)
(=> G D)
(=> H I)
(=> I (not D))
(=> (not D) I)
(=> C (not B))
C))

(apply ctx-solver-simplify)
; result: 
; (goals
; (goal
;  (=> A B)
;  (or (not D) E)
;  (or (not G) D)
;  (or (not H) I)
;  (or (not I) (not D))
;  (or D I)
;  (not B)
;  C
;  :precision precise :depth 1)
;)

对于您的实验，您可能需要查看策略 (http://rise4fun.com/z3/tutorialcontent/strategies#h21) 并在使用 API 之前在 SMT-LIB 界面中尝试一些，因为它可能会让您更快地进行实验。此外，如您所见，这会返回一个目标。在 Java API 中，尝试更改为以下内容并查看ApplyResult 对象的Subgoals 字段（这是Goal 对象的集合），看看它是否有你想要的：

Tactic simplifyTactic = ctx.mkTactic("ctx-solver-simplify");
Goal g = ctx.mkGoal();
g.Assert(bel2.toArray(new BoolExpr[0]));
ApplyResult a = simplifyTactic.Apply(g);
// look at a.Subgoals

这是基于我使用 .NET API 的经验，它可能与 Java 略有不同，但您可以在此处查看 Goal Java 文档： https://z3.codeplex.com/SourceControl/changeset/view/8bfbdf1e680d#src/api/java/Goal.java