CODEWITHSUNDEEP
z3smt
Nate
Nate

Reputation: 12849

Is it possible to use Z3 excluding SAT?

Z3 supports the SMT-lib set-logic statement to restrict to specific fragments. In a program using (set-logic QF_LRA) for example, quantifier-free linear real arithmetic is enabled. If multiple theories are enabled, it makes sense to me that SAT would be required. However, it's not clear to me if it's possible to enable a single theory and guarantee that SAT is never run, thereby reducing Z3 purely to a solver for that single theory alone. This would be useful for example to claim that a tool honors the particular performance bound of the solver for a given theory.

Is there a way to do this in SMT-lib, or directly in Z3? Or is guaranteeing that the SAT solver is disabled impossible?

Upvotes: 0

Views: 122

Answers (1)

alias
alias

Reputation: 30525

The Nelson-Oppen theory combination algorithm that many SMT solvers essentially implement crucially relies on the SAT solver: In a sense, the SAT solver is the engine that solves your SMT query, consulting the theory solvers to make sure the conflicts it finds are propagated/resolved according to the theory rules. So, it isn't really possible to talk about an SMT solver without an underlying SAT engine, and neither SMTLib nor any other tool I'm aware of allows you to "turn off" SAT. It's an integral piece of the whole system that cannot be turned on/off at will. Here's a nice set of slides for Nelson-Oppen: https://web.stanford.edu/class/cs357/lecture11.pdf

I suppose it would be possible to construct an SMT solver that did not use this architecture; but then every theory solver would need to essentially have a SAT solver embedded into itself. So, even in that scenario, extracting the "SAT" bits out is really not possible.

If you're after precise measurements of what part of the solver spends what amount of time, your best bet is to instrument the solver to collect statistics on where it spends its time. Even then, precisely calling which parts belong to the SAT solver, which parts belong to the theory solver, and which parts go to their combination will be tricky.

Upvotes: 3

Related Questions