z3 - Z3 中的 pb.conflict 是什么？

Question

我正在尝试使用Z3 APIfor python 找到最佳解决方案。我曾经打印过在检查 sat 时生成的set_option("verbose", 1)语句。Z3它打印的语句之一是pb.conflict语句。这些语句看起来像这样 -pb.conflict 语句。

我想知道pb.conflict到底是什么。这些陈述意味着什么？另外，与它一起打印的两个数字是什么？

标签： z3z3py

Answer 1

pb代表伪布尔值。伪布尔函数是从布尔值到其他域的函数，通常是Real. Aconflict发生在变量的选择导致无法满足的子句集时，此时求解器必须回溯。将回溯保持在最低限度对于提高效率至关重要，许多 SAT 引擎都会仔细跟踪该数字。虽然细节完全是求解器特定的（即，您要询问的这两个数字），但通常数字越大，求解器遇到的冲突案例越多，因此可能会决定完全重置状态或采取其他措施。通常，用户可以设置一些参数来指定何时采取这些行动以及这些行动究竟是什么。但同样，这完全是求解器和实现特定的。

谷歌搜索伪布尔优化会产生一堆你可能想要细读的学术文章。

如果您真的想找到 Z3 对伪布尔值的处理，那么您最好的选择可能是查看实现本身：https ://github.com/Z3Prover/z3/blob/master/src/smt/theory_pb.cpp