c++ - 跟踪 z3::optimize unsat_core
问题描述
如何正确跟踪z3::optimize
未饱和核心?
当我添加unsat_core跟踪(基于这些示例)(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;
}
另一方面,使用return跟踪 unsat_core ,这不是预期的解决方案。尽管如此,如果需要,我可以跟踪 unsat 核心 - 例如,添加会创建 unsat。问题。void add(expr const& e, expr const& t)
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;
}
使用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;
}
有趣的是,在上面的表达式中添加一个权重- 即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
,您现在可以使用第二次调用的结果。如果您有多个内核可供使用(现在谁没有?)这对最终用户来说应该几乎是透明的。
推荐阅读
- java - 从动态创建的 JTextField 中获取值
- wpf - 以编程方式设置时,讲述人不读取复选框状态
- json - Angular 5.2.10 - TypeScript 2.4.2 属性访问器 json 映射
- c# - C# EF6 映射未应用于选择
- python - 鲍鱼数据集准确率低
- c++ - 如何将单例类信号连接到主窗口类插槽或方法
- jenkins - Jenkins Build / Pipeline 作业 - 树中的作业列表 / 布局有序列表
- html - 将图像放在 HTML 中的文本上
- c++ - 包括没有标题的 SO 文件
- ruby-on-rails - 使用 link_to 将值写入属性