Calling external SAT solver from Z3

Question

In the company I work at, we have access to multiple SAT Solvers. We would like to analyze how each the SAT solvers affect the performance of the Z3 SMT solver.

Is it possible to call an external SAT solver from Z3? If not, where should the Z3 be modified to call an external solver?

Answer 1

I don't think this would be an easy task, because Z3 uses a tightly integrated internal SAT solver. The necessary tight integration with the SAT solver means that Z3 would have to interact via the low-level API of the external SAT solver, e.g. with push and pop functionality. These APIs are not standardized, so the task of integrating e.g. with MiniSat would be different than e.g. the task of integrating with Lingeling. I don't say it's not possible, because Z3 has a modular architecture that is meant to be extended, but I think this would be a major work effort.

It might be that one of the Z3 devs shows up and proves me wrong, though.