从 Z3 调用外部 SAT 求解器

【问题标题】：Calling external SAT solver from Z3从 Z3 调用外部 SAT 求解器
【发布时间】：2016-07-18 09:52:31
【问题描述】：

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

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

【问题讨论】：

标签： z3 smt sat

【解决方案1】：

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

不过，可能是 Z3 开发者之一出现并证明我错了。

【讨论】：