跟踪z3 ::优化unsat

问题描述

如何正确跟踪z3::optimize的非饱和核？

我添加 unsat_core 跟踪（基于这些examples）（gcc 10.1.0）时，Z3 C ++ z3::optimize未找到预期的解决方案。

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

下面的未跟踪代码提供了正确的解决方案。

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

#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 跟踪功能。

#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);，“强制”优化器找到正确的解决方案。

我在这里想念什么？

编辑：奇怪的是，如果我向优化器添加跟踪变量t[0-4]-即opt.add(ctx.bool_const("t0"));，依此类推，优化器会找到正确的解决方案，但会失去功能跟踪unsat核心表达式。考虑到我正在更改表达式的目的，这似乎很有意义。

解决方法

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

有关此问题的详细讨论，请参见以下主题：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，则可以使用第二个通话的结果。如果您有多个核心可供使用（这些天不是谁？），这对最终用户几乎是透明的。

c++z3

跟踪z3 ::优化unsat_core

问题描述

解决方法