获得新的 unsat 核心 [英] getting new unsat cores

问题描述

那里

我试图从公式中提取子句并每次更改一个子句的极性，如果已解决，则计算模型并将该子句放入集合中.如果解决了 unsat，则找出新的 unsat 核心.但是增量调用unsat core函数，即使解决了unsat，求解器也无法给出新的unsat cores.代码如下:

I am trying to extract clause from formulas and change one clause's polarity every time, if is solved sat, computing models and put the clause in the set. If it is solved unsat, then find out new unsat cores. But incrementally calling unsat core function, even it's solved unsat, the solver cannot give the new unsat cores. The codes as below:

context c;
expr x  = c.int_const("x");
expr y  = c.int_const("y");
solver s(c);
expr F  = x + y > 10 && x + y < 6 && y < 5 && x > 0;
assert(F.is_app());
vector<expr> qs;
if (F.decl().decl_kind() == Z3_OP_AND) {
    std::cout << "F num. args (before simplify): " << F.num_args() << "\n";
    F = F.simplify();
    std::cout << "F num. args (after simplify):  " << F.num_args() << "\n";
    for (unsigned i = 0; i < F.num_args(); i++) {
        std::cout << "Creating answer literal q" << i << " for " << F.arg(i) << "\n";
        std::stringstream qname; qname << "q" << i;
        expr qi = c.bool_const(qname.str().c_str()); // create a new answer literal
        s.add(implies(qi, F.arg(i)));
        qs.push_back(qi);
    }
}
qs.clear();
vector<expr> f,C,M;
size_t count = 0;
for(unsigned i=0; i<F.num_args(); i++){
    f.push_back(F.arg(i));
}
while(!f.empty() && count != F.num_args()){
    C.push_back(f[0]);
    f.erase(f.begin(),f.begin() +1);
    if(M.size()){
        for(unsigned i=0; i<f.size();i++){
            s.add(f[i]);
        }
        for(unsigned j=0; j<M.size(); j++){
            s.add(M[j]);
        }
        expr notC= to_expr(c, Z3_mk_not(c,C[count]));
        s.add(notC);
    }else{  
        expr notC = to_expr(c,Z3_mk_not(c,C[count]));
        s.add(notC);
        for(unsigned i =0; i<f.size(); i++){
            s.add(f[i]);
        }
    }
    if(s.check() == sat){
        cout<<"sat"<<"\n";
        M.push_back(C[count]);
    }else if(s.check() == unsat){
        size_t i;
        i=0;
        if(f.size()){
            for(unsigned w=0; w<f.size(); w++){
                std::stringstream qname;
                expr qi = c.bool_const(qname.str().c_str());
                s.add(implies(qi,f[w]));
                qs.push_back(qi);
                i++;
            }
        }
        for(unsigned j=0; j<M.size(); j++){
            stringstream qname;
            expr qi = c.bool_const(qname.str().c_str());
            s.add(implies(qi,M[j]));
            qs.push_back(qi);
            i++;
        }
        std::stringstream qname;
        expr qi = c.bool_const(qname.str().c_str());
        expr notC = to_expr(c,Z3_mk_not(c,C[count]));
        s.add(implies(qi,notC));
        if(s.check(qs.size(),&qs[0]) == unsat){
            expr_vector core2 = s.unsat_core();
            cout<<"new cores'size  "<<core2.size()<<endl;
            cout<<"new cores  "<<core2<<endl;
        }
    }
    qs.clear();
    count++;
}

推荐答案

目前还不清楚问题究竟是什么，但我猜您想从同一个公式中提取多个不同的未饱和核心.Z3 不支持开箱即用，但可以在其上实现算法.另请参阅之前的问题，尤其是那里给出的参考(计算最小不可满足约束子集的算法)，它解释了核心最小化背后的基础知识.

It's unclear what exactly the question is, but I'm guessing you would like to extract multiple different unsat cores from the same formula. Z3 does not support this out of the box, but algorithms can be implemented on top of it. See also this previous question and especially the reference given there (Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints), which explains the basics behind core minimization.

这篇关于获得新的 unsat 核心的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！