z3 - 从 Z3 调用外部 SAT 求解器

Question

在我工作的公司，我们可以使用多个 SAT Solver。我们想分析每个 SAT 求解器如何影响 Z3 SMT 求解器的性能。

是否可以从 Z3 调用外部 SAT 求解器？如果不是，应该在哪里修改 Z3 以调用外部求解器？

Answer 1

我认为这不是一件容易的事，因为 Z3 使用紧密集成的内部 SAT 求解器。与 SAT 求解器的必要紧密集成意味着 Z3 必须通过外部 SAT 求解器的低级 API 进行交互，例如与推送和弹出功能。这些 API 没有标准化，因此与 MiniSat 集成的任务与与 Lingeling 集成的任务不同。我并不是说这是不可能的，因为 Z3 有一个模块化架构，可以扩展，但我认为这将是一项重大的工作。

不过，可能是其中一位 Z3 开发人员出现并证明我错了。