Z3 Optimizer C++ API를 사용하여 실제 제약 조건으로 불만족 가능

Question

Z3 최적화 프로그램을 사용하여 그래프 분할 문제를 해결하려고 할 때 문제가 있습니다. 나는 minimize 명령을 제거하면

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

을하고 0 불균형 만족스러운 모델을 찾을 것이다 optimize 대신 solver를 사용 특히, 코드 우는 소리는 만족스러운 모델을 생산하기 위해 실패합니다.

1. 는 정수로 불균형 제한 환원 확인 제약 imbalance <= imbalance_limit 또는

2. 를 제거 : 나는 또한 어느 경우 optimize가 만족스러운 모델을 찾을 수 있습니다. 이 예에서 총 무게는 8입니다. 불균형 한도를 8/1, 8/2, 8/4 또는 8/8로 설정하면 옵티마이 저가 만족스러운 모델을 찾습니다.

나는 to_real(imbalance) <= imbalance_limit을 사용해 보았습니다. 나는 또한 Z3이 실수 논리에 대한 이론을 포함하지 않는 잘못된 논리를 사용하고있을 가능성을 고려했지만 C/C++ API를 사용하여이를 설정하는 방법을 찾지 못했습니다.

누가 내게 진정한 가치가있는 제약 조건 하에서 최적화가 실패했는지 또는 내 인코딩의 개선을 제안 할 수 있는지 말해 줄 수 있다면 많은 도움이 될 것입니다. 미리 감사드립니다.

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를 사용할 수 있습니다. 그런 식으로 무 건성 버그를 파는 것은 가능합니다 (그러나 쉬운 것은 아닙니다).