Z3/Java语言中的最优顶点覆盖

Question

如何在Z3/Java中编码下面的最优顶点覆盖问题？特别地，如何表达最小化条件？我在Z3/Java示例中找不到类似的示例。

(declare-fun vertex_a () Bool)
(declare-fun vertex_b () Bool)
(declare-fun vertex_c () Bool)
(declare-fun vertex_d () Bool)
(declare-fun vertex_e () Bool)
(declare-fun edge_a_c () Bool)
(declare-fun edge_a_b () Bool)
(declare-fun edge_a_e () Bool)
(declare-fun edge_b_c () Bool)
(declare-fun edge_b_d () Bool)
(declare-fun edge_b_e () Bool)
(assert edge_a_c)
(assert edge_a_b)
(assert edge_a_e)
(assert edge_b_c)
(assert edge_b_d)
(assert edge_b_e)
(assert (=> edge_a_c (or vertex_a vertex_c)))
(assert (=> edge_a_b (or vertex_a vertex_b)))
(assert (=> edge_a_e (or vertex_a vertex_e)))
(assert (=> edge_b_c (or vertex_b vertex_c)))
(assert (=> edge_b_d (or vertex_b vertex_d)))
(assert (=> edge_b_e (or vertex_b vertex_e)))
(minimize (+ (if vertex_a 1 0) (if vertex_b 1 0) (if vertex_c 1 0) (if vertex_d 1 0) (if vertex_e 1 0)))
(check-sat)
(get-model)

Answer 1

我弄明白了(参见下面的相关部分)。不需要求解器，而是使用Optimize。property包含含义，minimize_expr包含“真”顶点的总和。对于其他示例，我还必须从minimize_expr中删除未连接顶点的术语(if vertex_X 1 0)。

        Optimize optimize = context.mkOptimize();
        optimize.Add(property);
        optimize.MkMinimize(minimize_expr);
        optimize.Check();
        Model model = optimize.getModel();