c++ - Z3 Optimizer Unsatisfiability with Real Constraints Using C++ API

Question

我在尝试使用 Z3 优化器解决图形分区问题时遇到了问题。具体来说，下面的代码将无法生成令人满意的模型:

namespace z3 {
    expr ite(context& con, expr cond, expr then_, expr else_) {
        return to_expr(con, Z3_mk_ite(con, cond, then_, else_));;
    }
}

bool smtPart(void) {

    // Graph setup

    vector<int32_t> nodes = {{ 4, 2, 1, 1 }};
    vector<tuple<node_pos_t, node_pos_t, int32_t>> edges;
    GraphType graph(nodes, edges);

    // Z3 setup
    z3::context con;
    z3::optimize opt(con);
    string n_str = "n", sub_p_str = "_p";

    // Re-usable constants
    z3::expr zero = con.int_val(0);

    // Create the sort representing the different partitions.

    const char* part_sort_names[2] = { "P0", "P1" };
    z3::func_decl_vector part_consts(con), part_preds(con);

    z3::sort part_sort =
        con.enumeration_sort("PartID",
                             2,
                             part_sort_names,
                             part_consts,
                             part_preds);

    // Create the constants that represent partition choices.

    vector<z3::expr> part_vars;
    part_vars.reserve(graph.numNodes());

    z3::expr p0_acc = zero,
             p1_acc = zero;

    typename GraphType::NodeData total_weight = typename GraphType::NodeData();
    for (const auto& node : graph.nodes()) {
        total_weight += node.data;

        ostringstream name;
        name << n_str << node.id << sub_p_str;

        z3::expr nchoice = con.constant(name.str().c_str(), part_sort);
        part_vars.push_back(nchoice);

        p0_acc = p0_acc + z3::ite(con,
                                  nchoice == part_consts[0](), 
                                  con.int_val(node.data),
                                  zero);

        p1_acc = p1_acc + z3::ite(con,
                                  nchoice == part_consts[1](),
                                  con.int_val(node.data),
                                  zero);
    }

    z3::expr imbalance = con.int_const("imbalance");
    opt.add(imbalance ==
            z3::ite(con,
                    p0_acc > p1_acc,
                    p0_acc - p1_acc,
                    p1_acc - p0_acc));

    z3::expr imbalance_limit = con.real_val(total_weight, 100);
    opt.add(imbalance <= imbalance_limit);

    z3::expr edge_cut = zero;
    for(const auto& edge : graph.edges()) {
        edge_cut = edge_cut +
                   z3::ite(con,
                           (part_vars[edge.node0().pos()] ==
                              part_vars[edge.node1().pos()]),
                           zero,
                           con.int_val(edge.data));
    }

    opt.minimize(edge_cut);
    opt.minimize(imbalance);

    z3::check_result opt_result = opt.check();

    if (opt_result == z3::check_result::sat) {
        auto mod = opt.get_model();

        size_t node_id = 0;
        for (z3::expr& npv : part_vars) {
            cout << "Node " << node_id++ << ": " << mod.eval(npv) << endl;
        }

        return true;
    } else if (opt_result == z3::check_result::unsat) {
        cerr << "Constraints are unsatisfiable." << endl;
        return false;
    } else {
        cerr << "Result is unknown." << endl;
        return false;
    }
}

如果我删除 minimize命令并使用 solver而不是 optimize它会找到一个令人满意的 0 失衡模型。我也可以得到 optimize找到一个令人满意的模型，如果我:

1. 移除约束imbalance <= imbalance_limit或者

2. 使不平衡限制可简化为整数。在此示例中，总权重为 8。如果将不平衡限制设置为 8/1、8/2、8/4 或 8/8，优化器将找到令人满意的模型。

我试过了to_real(imbalance) <= imbalance_limit无济于事。我还考虑了 Z3 使用错误逻辑(不包括实数理论的逻辑)的可能性，但我还没有找到使用 C/C++ API 进行设置的方法。

如果有人能告诉我为什么优化器在存在实值约束的情况下失败，或者可以建议改进我的编码，我们将不胜感激。提前致谢。

Answer 1

您能否通过使用 opt.to_string() 转储状态(就在 check() 之前)来重现结果？这将创建一个带有优化命令的 SMT-LIB2 格式的字符串。这样就更容易交换基准。如果您注释掉优化命令，您应该会看到它报告对优化命令不满意和满意。

如果您能够产生错误，请在 GitHub.com/z3prover/z3.git 上发布问题并进行重现。

如果没有，您可以在创建 z3 上下文并记录可重新运行的日志文件之前使用 Z3_open_log。以这种方式挖掘不健全的错误是可能的(但不是那么容易)。