java - Z3:使用Java API来简化断言

Question

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

我正在尝试使用简化来获取有关断言集中冗余信息的知识。

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

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(不是 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();

这样做会产生一个模型，而不是简化。此外，对我来说，让简化策略发挥作用有点困难。通常结果是未知的，原因是“不完整”。

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

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

Answer 1

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

使用简化策略更符合您的需求，但您可能需要应用不同的策略来实现您想要的转换。但是，当我以 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