Z3 Optimizer C++ APIを使用した実数制約の不確かさ

Question

Z3オプティマイザを使用してグラフの分割問題を解決しようとすると問題が発生しています。私はminimizeコマンドを削除し、それが0不均衡と満足のいくモデルを見つける代わりにoptimizeのsolverを使用する場合は

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; 
    } 
} 

：具体的には、コード怒鳴るは満足のいくモデルを生成するために失敗します。

1. imbalance <= imbalance_limitまたは

2. が整数に不均衡制限が還元可能作る制約を削除します。私もどちらかがあればoptimizeは満足のいくモデルを見つけるために取得することができます。この例では合計重量は8です。不均衡の制限が8/1、8/2、8/4、または8/8に設定されている場合、オプティマイザは満足できるモデルを見つけます。

私はto_real(imbalance) <= imbalance_limitを無駄にしようとしました。私はまた、Z3が誤ったロジック（実数の理論を含まないロジック）を使用している可能性を考えましたが、C/C++ APIを使用してZ3を設定する方法が見つかりませんでした。

本当の価値のある制約の下でオプティマイザが失敗したり、エンコーディングが改善された理由を教えていただけたら、前もって感謝します。

Answer 1

これはZ3のバグであることが判明しました。私はGitHubでIssueを作成し、その後パッチで対応してきました。私は今コンパイルしてテストをテストしていますが、動作することを期待しています。

編集：はい、そのパッチは、コマンドラインツールとC++ APIの問題を修正しました。

Answer 2

opt.to_string（）を使用して状態をダンプする（check（）の直前）結果を再現できますか？これにより、最適化コマンドを使用してSMT-LIB2でフォーマットされた文字列が作成されます。ベンチマークを交換する方が簡単です。最適化コマンドでunsatが報告され、最適化コマンドをコメントアウトすると表示されるはずです。

バグを生成できる場合は、GitHub.com/z3prover/z3.gitにレシピを投稿してください。

もしそうでなければ、z3コンテキストを作成して再実行可能なログファイルを記録する前に、Z3_open_logを使用することができます。そういう意味では、無傷のバグを掘り下げることは可能です（しかし簡単ではありません）。