将子句直接添加到 z3 求解器
Adding clauses directly to the z3 solver
我有一个 AIG（和逆变器图），我一直在修改它，我需要使用 Z3 以增量方式检查它的可满足性。我可以生成 AIG 的 CNF 表示，理想情况下，我希望将这些子句直接提供给求解器，并从我的代码中重复调用它。有什么方法可以通过 C/C++ API 直接向 Z3 求解器添加子句（或 AIG）？
是的，您可以简单地断言新的断言，这些断言在内部被翻译成子句。
请注意，对于许多增量求解问题，Z3 不使用现成的专用 SAT 求解器，而是使用自己的 SMT 求解器，它结合了 SAT 求解器的一些功能，但不是全部，并且本机处理非布尔问题。因此，破解求解器直接注入子句不一定会转化为显着提高的性能。
Z3 也有一个专用的纯布尔 SAT 求解器，如果您正在求解纯布尔问题，这个求解器可能会快得多。您可以通过将 (check-sat) 替换为 (check-sat-using sat) 或通过 运行 称为 'sat' 的策略来强制它使用此求解器。此求解器的实现在 sat_solver.h/.cpp 中，如果您想破解它，这将是开始四处看看的主要地方。
Z3 还使用它自己的 AIG 实现作为某些策略中的预处理步骤，请参阅 aig_tactic.h/.cpp。
我有一个 AIG（和逆变器图），我一直在修改它，我需要使用 Z3 以增量方式检查它的可满足性。我可以生成 AIG 的 CNF 表示，理想情况下，我希望将这些子句直接提供给求解器，并从我的代码中重复调用它。有什么方法可以通过 C/C++ API 直接向 Z3 求解器添加子句（或 AIG）？
是的，您可以简单地断言新的断言，这些断言在内部被翻译成子句。
请注意，对于许多增量求解问题，Z3 不使用现成的专用 SAT 求解器，而是使用自己的 SMT 求解器，它结合了 SAT 求解器的一些功能，但不是全部，并且本机处理非布尔问题。因此，破解求解器直接注入子句不一定会转化为显着提高的性能。
Z3 也有一个专用的纯布尔 SAT 求解器，如果您正在求解纯布尔问题，这个求解器可能会快得多。您可以通过将 (check-sat) 替换为 (check-sat-using sat) 或通过 运行 称为 'sat' 的策略来强制它使用此求解器。此求解器的实现在 sat_solver.h/.cpp 中，如果您想破解它，这将是开始四处看看的主要地方。
Z3 还使用它自己的 AIG 实现作为某些策略中的预处理步骤，请参阅 aig_tactic.h/.cpp。