跟踪 z3::优化 unsat_core [英] Tracking z3::optimize unsat_core

问题描述

如何正确跟踪 z3::optimize 未饱和内核?

How to properly track z3::optimize unsat core?

当我添加 unsat_core 跟踪时，Z3 C++ z3::optimize 没有找到预期的解决方案(基于这些 examples) (gcc 10.0).

The Z3 C++ z3::optimize does not find the expected solution when I add unsat_core tracking (based on these examples) (gcc 10.1.0).

考虑如下问题:有三个连续的点A、B和C，其中A和 C 分别固定为 0 和 200.确定B的位置，使得B - A >= 10，C - B >= 15，我们的优化目标是<代码>最小化(C - B).这个问题的解应该是B = C - 15 = 200 - 15 = 185.

Take the following problem: There are three consecutive points A, B, and C, where A and C are fixed to 0 and 200, respectively. Determine B's position such that B - A >= 10, C - B >= 15, and our optimization goal is minimize(C - B). The solution for this problem should be B = C - 15 = 200 - 15 = 185.

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

The untracked code below gives the correct solution.

#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，这不是期望的解决方案.尽管如此，如果需要，我可以跟踪 unsat 核心 - 例如添加 opt.add(ctx.int_const("B") == 200, ctx.bool_const("t4")); 创建一个 unsat.问题.

On the other hand, tracking the unsat_core with void add(expr const& e, expr const& t) return B=10, which is not the expect solution. Nonetheless, I am able to track the unsat core if need - e.g. adding opt.add(ctx.int_const("B") == 200, ctx.bool_const("t4")); creates an unsat. problem.

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

使用 z3::implies 跟踪表达式也不能按预期工作，但仍提供 unsat_core 跟踪功能.

Using z3::implies to track expressions does not work as expected either, but still provides unsat_core tracking capability.

#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 - 即 handle add(expr const& e, unsigned weight) - 例如opt.add(z3::implies(ctx.bool_const("t0"), ctx.int_const("A") == 0), 1);, "forces"优化器以达到正确的解决方案.

Interestingly, adding a weight - i.e. handle add(expr const& e, unsigned weight) - to the expressions above - e.g. opt.add(z3::implies(ctx.bool_const("t0"), ctx.int_const("A") == 0), 1);, "forces" the optimizer to reach the correct solution.

我在这里遗漏了什么?

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

Curiously, if I add tracking variables t[0-4] to the optimizer - i.e. opt.add(ctx.bool_const("t0")); and so on, the optimizer finds the correct solution, but it loses the capability of tracking the unsat core expressions. That seems to make sense, considering I am changing the expression's purpose.

推荐答案

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

z3 doesn't support unsat-cores in the optimization mode.

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

See this thread for a detailed discussion of this issue: https://github.com/Z3Prover/z3/issues/1577

推荐的解决方案(伪代码)是:

The recommended solution (in pseudo-code) is:

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，您现在可以使用第二次调用的结果.如果您有多个内核可供您使用(现在谁没有?)这对最终用户几乎是透明的.

Admittedly, this isn't ideal; but that's the current state of the implementation. If this feature is important to you, I recommend filing a ticket with z3 as a feature-request, though without a convincing use case it's unlikely to be implemented. A better option for you might be to use parallelization capabilities in your host language: Start two threads, one with regular sat call, and one with optimization. If you get unsat, kill the second and get the unsat-core from the first. If you get sat, you can now use the results of your second call. If you have multiple cores at your disposal (who doesn't these days?) this should be almost transparent to the end-user.

这篇关于跟踪 z3::优化 unsat_core的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！