c++ - 关于如何让 Z3 更快地评估简单约束的建议

Question

我正在尝试使用 Z3（带有 C++ API）来检查大量变量配置是否满足我的约束，但我遇到了很大的性能问题。

我正在寻找关于我可以使用哪些逻辑或参数设置来改进运行时的建议，或者关于我如何尝试以不同的方式将问题反馈给 Z3 的提示。

我在做什么以及如何做的简短描述：

//_______________Pseudocode and example_______________

context ctx()
solver s(ctx)

// All my variables are finite domain, maybe some 20 values at most, but usually less. 
// They can only be ints, bools, or enums. 
// There are not that many variables, maybe 10 or 20 for now.
//
// Since I need to be able to solve constraints of the type (e == f), where
// e and f are two different enum variables, all my
// enum types are actually contained in only one enumeration_sort(), populated
// with all the different values.

sort enum_sort = {"green", "red", "yellow", "blue", "null"}

expr x = ctx.int_const("x")
expr y = ctx.int_const("y")
expr b = ctx.bool_const("b")
expr e = ctx.constant("e", enum_sort)
expr f = ctx.constant("f", enum_sort)

// now I assert the finite domains, for each variable
// enum_value(s) is a helper function, that returns the matching enum expression
//
// Let's say that these are the domains:
//
// int x is from {1, 3, 4, 7, 8}
// int y is from {1, 2, 3, 4}
// bool b is from {0, 1}
// enum e is from {"green", "red", "yellow"}
// enum f is from {"red", "blue", "null"}

s.add(x == 1 || x == 3 || x == 3 || x == 7 || x == 8)
s.add(y == 1 || y == 2 || y == 3 || y == 4)
s.add(b == 0 || b == 1)
s.add(e == enum_value("green") || e == enum_value("red") || enum_value("yellow"))
s.add(f == enum_value("red") || f == enum_value("blue") || enum_value("null"))

// now I add in my constraints. There are also about 10 or 20 of them, 
// and each one is pretty short

s.add(b => (x + y >= 5))
s.add((x > 1) => (e != f))
s.add((y == 4 && x == 1) || b)

// setup of the solver is now done. Here I start to query different combinations
// of values, and ask the solver if they are "sat" or "unsat"
// some values are left empty, because I don't care about them
expr_vector vec1 = {x == 1, y == 3, b == 1, e == "red"}
print(s.check(vec1))

expr_vector vec2 = {x == 4, e == "green", f == "null"}
print(s.check(vec2))

....

// I want to answer many such queries.

当然，就我而言，这不是硬编码的，但我从文件中读取并解析约束、变量及其域，然后将信息提供给 Z3。

但它很慢。

即使是一万个查询，我的程序也已经运行了 10 多秒。所有这些都在 s.check() 中。有没有可能让它跑得更快？

希望是这样，因为我对求解器的要求看起来并不太难。没有量词，有限域，没有函数，一切都是整数或枚举，域很小，数字的值很小，只有简单的算术，约束很短等等。

如果我尝试使用参数进行并行处理，或者将逻辑设置为“QF_FD”，则运行时根本不会改变。

提前感谢您的任何建议。

标签： c++performanceoptimizationconstraintsz3

Answer 1

总是很慢吗？或者当您使用相同的求解器查询越来越多的配置时，它是否会变得越来越慢？

如果是前者，那么你的问题就太难了，这是要付出的代价。我认为您所展示的内容没有任何明显错误；尽管您永远不应该将布尔值用作整数。（只需查看您的b变量。坚持将布尔值作为布尔值，将整数作为整数，除非您真的必须这样做，否则不要将两者混合在一起。有关这一点的进一步说明，请参阅此答案：为什么 Z3 慢对于微小的搜索空间？）

如果是后者，您可能希望为每个查询从头开始创建求解器，以清理求解器创建的所有额外内容。虽然额外的引理总是有帮助，但如果求解器在后续查询中不能很好地利用它们，它们也可能会损害性能。如果您遵循这条路径，那么您可以简单地在您的 C++ 程序中自己“并行化”问题；即，为每个问题创建多个线程并分别调用求解器，充分利用您的计算机无疑拥有的多核和操作系统级别的多任务处理。

诚然，这是非常笼统的建议，可能并不直接适用于您的情况。但是，如果没有我们可以看到和检查的特定“运行”示例，很难比这更具体。