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

Question

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

Answer 1

是的，您可以简单地断言新的断言，这些断言在内部被翻译成子句。

请注意，对于许多增量求解问题，Z3 不使用现成的专用 SAT 求解器，而是它自己的 SMT 求解器，它结合了 SAT 求解器的一些功能，但不是全部，并且本机处理非布尔问题。因此，破解求解器直接注入子句不一定会转化为显着提高的性能。

Z3 还有一个专门的纯布尔型 SAT 求解器，如果您要求解纯布尔型问题，这个求解器可能要快得多。(check-sat)您可以通过替换为(check-sat-using sat)或运行名为“sat”的策略来强制它使用此求解器。这个求解器的实现在sat_solver.h/.cpp，如果你想破解它，这将是开始环顾四周的主要地方。

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