有关如何使 Z3 更快地评估简单约束的建议
Advice about how to make Z3 evaluate simple constraints faster
我正在尝试使用 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。
但是很慢。
即使是一万个查询，我的程序也已经 运行ning 超过 10 秒。所有这些都在 s.check() 中。有可能让它 运行 更快吗？
希望是这样，因为我对求解器的要求看起来并不过分困难。
没有量词，有限域，没有函数，一切都是整数或枚举，域很小，数字的值很小，只有简单的算术，约束很短，等等。
如果我尝试使用参数进行并行处理，或者将逻辑设置为"QF_FD"，运行时间根本不会改变。
提前感谢您的任何建议。
总是很慢吗？还是随着您使用同一个求解器查询越来越多的配置，它会变得越来越慢？
如果是前者，那么你的问题太难了，这就是你要付出的代价。我没有看到你所展示的任何明显错误；尽管您永远不应该将布尔值用作整数。 （只是看看你的 b 变量。坚持布尔值作为布尔值，整数作为整数，除非你真的必须，否则不要将两者混合在一起。有关这一点的进一步阐述，请参阅此答案: )
如果是后者，您可能希望从头开始为每个查询创建一个求解器，以清除求解器创建的所有额外内容。虽然额外的引理总是有帮助的，但如果求解器不能在后续查询中充分利用它们，它们也会损害性能。如果你遵循这条道路，那么你可以简单地 "parallelize" 在你的 C++ 程序中自己解决问题；即，创建多个线程并针对每个问题分别调用求解器，充分利用您的计算机无疑拥有的多核和 OS 级多任务处理能力。
诚然，这是非常笼统的建议，可能并不直接适用于您的情况。但是，如果没有我们可以看到和检查的特定 "running" 示例，很难比这个更具体。
一些想法：
1. 将 x == 1 || x == 3 || x == 3 || x == 7 || x == 8 替换为 (1 <= x && x <= 8) && (x <= 1 || (3 <= x) && (x <= 4 || 7 <= x)。 y 的类似更改。
基本原理： 线性算术的求解器现在知道 x 总是限制在区间 [1,8] 内，这对于其他线性算术可能是有用的信息equalities/inequalities;学习简单的互斥约束 not(x <= 1) || not(3 <= x) 和 not(x <= 4) || not(7 <= x) 可能也很有用；现在恰好有 3 个布尔赋值覆盖了您原来的 5 个案例，这使得线性算术求解器的推理更具成本效益，因为每次调用都会处理更大的搜索块 space. （此外，从冲突中学到的子句更有可能对后续调用求解器有用）
（您的查询可能还包含一组值，而不是特定的值分配；这可能允许人们用更少的查询来修剪一些无法满足的值范围）
2. 正如@alias 提到的，布尔变量应该是布尔值而不是 0/1 整数变量。您提供的示例有点令人困惑， b 被声明为 bool const 但随后您声明 b == 0 || b == 1
3.我不熟悉z3的enum_sort，意思就是不知道怎么回事内部编码以及应用什么解决技术来处理它。因此，我不确定求解器是否会尝试生成不一致的真值分配，其中 e == enum_value("green") 和 e == enum_value("red") 同时分配给 true。这可能值得进行一些调查。例如，另一种可能性是将 e 和 f 声明为 Int 并使用 中所示的相同方法为它们提供适当的间隔域（尽可能连续） 1.，您的软件会将其解释为 enum 值的列表。这应该从搜索中删除一些布尔赋值 space，使冲突子句更有效并可能加快搜索速度。
4. 鉴于问题变量、值和约束的数量很少，我建议您尝试仅使用位向量理论对所有内容进行编码仅此而已（使用小而大的域）。如果您随后将求解器配置为编码位向量 eagerly，那么所有内容都会被位爆破到 SAT 中，并且 z3 应该只使用布尔约束传播来实现可满足性，这是最便宜的技术。
这可能是一个 X Y 问题，你为什么要执行数千个查询，你想达到什么目的？您是否正在尝试探索所有可能的值组合？您要执行模型计数吗？
我正在尝试使用 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。
但是很慢。
即使是一万个查询，我的程序也已经 运行ning 超过 10 秒。所有这些都在 s.check() 中。有可能让它 运行 更快吗？
希望是这样，因为我对求解器的要求看起来并不过分困难。 没有量词，有限域，没有函数，一切都是整数或枚举，域很小，数字的值很小，只有简单的算术，约束很短，等等。
如果我尝试使用参数进行并行处理，或者将逻辑设置为"QF_FD"，运行时间根本不会改变。
提前感谢您的任何建议。
总是很慢吗？还是随着您使用同一个求解器查询越来越多的配置，它会变得越来越慢？
如果是前者，那么你的问题太难了，这就是你要付出的代价。我没有看到你所展示的任何明显错误；尽管您永远不应该将布尔值用作整数。 （只是看看你的 b 变量。坚持布尔值作为布尔值，整数作为整数，除非你真的必须，否则不要将两者混合在一起。有关这一点的进一步阐述，请参阅此答案:
如果是后者，您可能希望从头开始为每个查询创建一个求解器，以清除求解器创建的所有额外内容。虽然额外的引理总是有帮助的，但如果求解器不能在后续查询中充分利用它们，它们也会损害性能。如果你遵循这条道路，那么你可以简单地 "parallelize" 在你的 C++ 程序中自己解决问题；即，创建多个线程并针对每个问题分别调用求解器，充分利用您的计算机无疑拥有的多核和 OS 级多任务处理能力。
诚然，这是非常笼统的建议，可能并不直接适用于您的情况。但是，如果没有我们可以看到和检查的特定 "running" 示例，很难比这个更具体。
一些想法：
1. 将
x == 1 || x == 3 || x == 3 || x == 7 || x == 8替换为(1 <= x && x <= 8) && (x <= 1 || (3 <= x) && (x <= 4 || 7 <= x)。y的类似更改。基本原理： 线性算术的求解器现在知道
x总是限制在区间[1,8]内，这对于其他线性算术可能是有用的信息equalities/inequalities;学习简单的互斥约束not(x <= 1) || not(3 <= x)和not(x <= 4) || not(7 <= x)可能也很有用；现在恰好有3个布尔赋值覆盖了您原来的5个案例，这使得线性算术求解器的推理更具成本效益，因为每次调用都会处理更大的搜索块 space. （此外，从冲突中学到的子句更有可能对后续调用求解器有用）（您的查询可能还包含一组值，而不是特定的值分配；这可能允许人们用更少的查询来修剪一些无法满足的值范围）
2. 正如@alias 提到的，布尔变量应该是布尔值而不是 0/1 整数变量。您提供的示例有点令人困惑，
b被声明为 bool const 但随后您声明b == 0 || b == 13.我不熟悉
z3的enum_sort，意思就是不知道怎么回事内部编码以及应用什么解决技术来处理它。因此，我不确定求解器是否会尝试生成不一致的真值分配，其中e == enum_value("green")和e == enum_value("red")同时分配给true。这可能值得进行一些调查。例如，另一种可能性是将e和f声明为Int并使用 中所示的相同方法为它们提供适当的间隔域（尽可能连续） 1.，您的软件会将其解释为enum值的列表。这应该从搜索中删除一些布尔赋值 space，使冲突子句更有效并可能加快搜索速度。4. 鉴于问题变量、值和约束的数量很少，我建议您尝试仅使用位向量理论对所有内容进行编码仅此而已（使用小而大的域）。如果您随后将求解器配置为编码位向量 eagerly，那么所有内容都会被位爆破到 SAT 中，并且
z3应该只使用布尔约束传播来实现可满足性，这是最便宜的技术。
这可能是一个 X Y 问题，你为什么要执行数千个查询，你想达到什么目的？您是否正在尝试探索所有可能的值组合？您要执行模型计数吗？