CODEWITHSUNDEEP
c++z3
delirium
delirium

Reputation: 918

Tracking z3::optimize unsat_core

How to properly track z3::optimize unsat core?

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).

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

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

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

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.

What am I missing here?

EDIT: 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.

Upvotes: 2

Views: 170

Answers (1)

alias
alias

Reputation: 30485

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

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

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.

Upvotes: 1

Related Questions