CODEWITHSUNDEEP
algorithmz3solversmtsat
Lance Pollard
Lance Pollard

Reputation: 79458

Algorithms behind the z3 solver

I just learned about DPLL(T) and the DPLL algorithm in relation to SMT solvers. I have seen z3 referenced in a few places regarding SMT solvers as well.

Wondering what the z3 uses for its algorithms at a high level for implementing the SMT solving. If it is DPLL algorithms, a variation, something custom, a bunch of things, etc. Hoping to learn about the different types of algorithms a modern SMT solver uses.

Upvotes: 1

Views: 965

Answers (2)

AmirHosein Sadeghimanesh
AmirHosein Sadeghimanesh

Reputation: 478

You can check the following link where it says what algorithms are used in Z3 and many more stuff. For example in section 6.5 you can see that they use NLSAT algorithm for nonlinear real arithmetic theory parts. https://theory.stanford.edu/~nikolaj/programmingz3.html

Upvotes: 3

alias
alias

Reputation: 30525

SMT solvers come from a long line of research in automated reasoning, both in computer-based theorem-proving communities and in traditional mathematical logic. It's impossible to summarize all the algorithms/research in a stack-overflow answer. However, the book http://www.decision-procedures.org/ is an excellent read, and have many references that can help you guide into the literature. (The first edition is already 10 years old, but I see now that they have a second edition that came out in 2016.)

Upvotes: 3

Related Questions