Z3：差分逻辑性能

Question

我有一个问题要解决，可以转化为不同的逻辑，而不是实施决策程序，我想使用 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;
}

非常感谢，

佩德罗

Answer 1

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

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

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

Z3：差分逻辑性能

Z3: Difference logic performance

logic

z3

difference