Z3：差分逻辑性能答案

【问题标题】：Z3: Difference logic performanceZ3：差分逻辑性能
【发布时间】：2015-05-18 01:17:16
【问题描述】：

我有一个可以转化为差异逻辑的问题要解决，我想使用 z3 来实现此目的，而不是执行决策过程。尽管如此，我运行了一些示例并且我有类似指数的运行时（即使它有一个多时间决策过程）。我是 z3 的新手，我不知道我是否做错了什么。这是我正在使用的代码（c++ api），改变这个“max”变量。

int main(int argc, char **argv) {
context c;

solver s(c, "QF_IDL");

int max = 10000;
int prev = 0;
for(int i = 1; i < max; ++i){
    expr x = s.ctx().int_const(std::to_string(i).c_str());
    expr y = s.ctx().int_const(std::to_string(++i).c_str());
    expr pr = s.ctx().int_const(std::to_string(prev).c_str());
    s.add(pr < x);
    s.add(x < y);
    prev = i;
}

s.add(s.ctx().int_const(std::to_string(max-1).c_str()) < s.ctx().int_const(std::to_string(0).c_str()));

clock_t begin = clock();
switch (s.check()) {
    case unsat:   std::cout << "UNSAT"; break;
    case sat:     std::cout << "SAT"; break;
    case unknown: std::cout << "unknown\n"; break;
}

clock_t end = clock();
double elapsed_secs = double(end - begin) / CLOCKS_PER_SEC;

std::cout << "elapsed time: " << elapsed_secs;
}

非常感谢，

佩德罗

【问题讨论】：

标签： logic z3 difference

【解决方案1】：

默认情况下，Z3 使用单工引擎，有时甚至使用 Floyd Marshall 引擎来解决您的约束，即使逻辑是 QF_IDL。在这种情况下，它使用单纯形引擎，并且对于此示例，行的大小呈二次方增长。您可以通过在您的程序中插入以下内容来强制使用稀疏差分逻辑求解器：

 params p(c);
 p.set("auto_config", false);
 p.set("smt.arith.solver", (unsigned)1);
 solver s(c, "QF_IDL");
 s.set(p);

这会将算术求解器设置为稀疏差分逻辑求解器。它不受空间开销的影响。它仍然需要二次方时间，或更准确地说，时间与 |V||E| 成正比其中|V|是数字变量和|E|是不等式的数量。在这种情况下，主要的时间瓶颈是大数算法，这不是在你的情况下是必要的。我为 Z3 的不稳定分支添加了更新，以便它识别仅使用小整数的场景，以便它可以使用更有效的表示。这需要将较大示例的时间减少约 5 倍。尽管如此，开销仍然是 |V||E|。

【讨论】：