c++ - 直接将子句添加到 z3 求解器

Question

我有一个 AIG(和逆变器图)，我不断修改它，并且我需要使用 Z3 以增量方式检查其可满足性。我可以生成 AIG 的 CNF 表示，并且理想情况下希望将这些子句直接提供给求解器并从我的代码中重复调用它。有什么方法可以通过 C/C++ API 直接向 Z3 求解器添加子句(或 AIG)吗？

Answer 1

是的，您可以简单地断言新断言，这些断言在内部转换为子句。

请注意，对于许多增量求解问题，Z3 不使用现成的专用 SAT 求解器，而是它自己的 SMT 求解器，该求解器包含 SAT 求解器的一些功能(但不是全部)，并且它本身可以处理非 bool 问题。因此，破解求解器直接注入(inject)子句并不一定会显着提高性能。

Z3 还有一个专用的纯 bool SAT 求解器，如果您要解决纯 bool 问题，该求解器可能会快得多。您可以通过将 (check-sat) 替换为 (check-sat-using sat) 或运行名为“sat”的策略来强制它使用此求解器。该求解器的实现位于 sat_solver.h/.cpp ，如果您想破解它，这将是开始四处寻找的主要位置。

Z3 还使用其自己的 AIG 实现作为某些策略中的预处理步骤，请参阅 aig_tactic.h/.cpp .