跟踪 z3::optimize unsat_core

如何正确追踪z3::optimize未饱和核心？

Z3 C++z3::optimize当我添加时没有找到预期的解决方案不饱和核心跟踪（基于这些examples https://github.com/Z3Prover/z3/blob/9df6c10ad87ae37c7deba1e7428496dbd5ab0022/examples/c%2B%2B/example.cpp#L395）（海湾合作委员会10.1.0）。

拿下面的问题：有三个连续的点A, B, and C, where A and C分别固定为 0 和 200。决定B的位置使得B - A >= 10, C - B >= 15，我们的优化目标是minimize(C - B)。这个问题的解决方案应该是B = C - 15 = 200 - 15 = 185.

The 下面未跟踪的代码给出了正确的解决方案。

#include <iostream>
#include <z3++.h>

int main()
{
  z3::context ctx;
  z3::optimize opt(ctx);

  opt.add(ctx.int_const("A") == 0);
  opt.add(ctx.int_const("B") - ctx.int_const("A") >= 10);
  opt.add(ctx.int_const("C") - ctx.int_const("B") >= 15);
  opt.add(ctx.int_const("C") == 200);

  auto h = opt.minimize(ctx.int_const("C") - ctx.int_const("B"));

  if (opt.check() != z3::sat)
    std::cout << "unsat problem!\n" << opt.unsat_core() << std::endl;
  else
    std::cout << "model!\n" << opt.get_model() << std::endl;

  return 0;
}

另一方面，跟踪 unsat_core void add(expr const& e, expr const& t) return B=10，这不是预期的解决方案。尽管如此，如果需要，我可以跟踪未饱和的核心 - 例如添加opt.add(ctx.int_const("B") == 200, ctx.bool_const("t4"));造成不饱和。问题。

#include <iostream>
#include <z3++.h>

int main()
{
  z3::context ctx;
  z3::optimize opt(ctx);

  opt.add(ctx.int_const("A") == 0, ctx.bool_const("t0"));
  opt.add(ctx.int_const("B") - ctx.int_const("A") >= 10, ctx.bool_const("t1"));
  opt.add(ctx.int_const("C") - ctx.int_const("B") >= 15, ctx.bool_const("t2"));
  opt.add(ctx.int_const("C") == 200, ctx.bool_const("t3"));

  auto h = opt.minimize(ctx.int_const("C") - ctx.int_const("B"));

  if (opt.check() != z3::sat)
    std::cout << "unsat problem!\n" << opt.unsat_core() << std::endl;
  else
    std::cout << "model!\n" << opt.get_model() << std::endl;

  return 0;
}

Using z3::implies跟踪表达式也没有按预期工作，但仍然提供不饱和核心跟踪能力。

#include <iostream>
#include <z3++.h>

int main()
{
  z3::context ctx;
  z3::optimize opt(ctx);

  opt.add(z3::implies(ctx.bool_const("t0"), ctx.int_const("A") == 0));
  opt.add(z3::implies(ctx.bool_const("t1"), ctx.int_const("B") - ctx.int_const("A") >= 10));
  opt.add(z3::implies(ctx.bool_const("t2"), ctx.int_const("C") - ctx.int_const("B") >= 15));
  opt.add(z3::implies(ctx.bool_const("t3"), ctx.int_const("C") == 200));

  auto h = opt.minimize(ctx.int_const("C") - ctx.int_const("B"));

  z3::expr_vector asv(ctx);
  asv.push_back(ctx.bool_const("t0"));
  asv.push_back(ctx.bool_const("t1"));
  asv.push_back(ctx.bool_const("t2"));
  asv.push_back(ctx.bool_const("t3"));

  if (opt.check(asv) != z3::sat)
    std::cout << "unsat problem!\n" << opt.unsat_core() << std::endl;
  else
    std::cout << "model!\n" << opt.get_model() << std::endl;

  return 0;
}

有趣的是，添加一个weight - i.e. handle add(expr const& e, unsigned weight)- 对于上面的表达式 - 例如opt.add(z3::implies(ctx.bool_const("t0"), ctx.int_const("A") == 0), 1);，“强制”优化器达到正确的解决方案。

我在这里缺少什么？

EDIT:奇怪的是，如果我添加跟踪变量t[0-4]到优化器 - 即opt.add(ctx.bool_const("t0"));依此类推，优化器找到了正确的解决方案，但失去了跟踪不饱和核心表达式的能力。考虑到我正在改变表达式的目的，这似乎是有道理的。

z3 在优化模式下不支持 unsat-cores。

有关此问题的详细讨论，请参阅此线程：https://github.com/Z3Prover/z3/issues/1577 https://github.com/Z3Prover/z3/issues/1577

推荐的解决方案（伪代码）是：

1.  Assert all constraints except optimization objectives
2.  Issue `check-sat`
        2.1 If `unsat`, get the unsat-core: done
        2.2 If `sat`:
              2.2.1 Assert the optimization objectives
              2.2.2 Issue `check-sat` again
              2.2.3 Get objective values

诚然，这并不理想。但这就是目前的实施情况。如果此功能对您很重要，我建议使用 z3 提交票据作为功能请求，但如果没有令人信服的用例，则不太可能实现。对您来说，更好的选择可能是使用宿主语言中的并行化功能：启动两个线程，其中一个使用常规线程sat打电话，一个与optimization。如果你得到unsat，杀死第二个并从第一个中获取 unsat-core。如果你得到sat，您现在可以使用第二次调用的结果。如果您有多个核心可供使用（现在谁没有？），这对最终用户来说几乎是透明的。