CODEWITHSUNDEEP
z3
Anon
Anon

Reputation: 421

References for Z3 - how does it work[internal theory]?

I am interested in reading the internal theory behind Z3. Specifically I want to read, how Z3 SMT solver works, and how it is able to find counterexamples for an incorrect model. I wish to be able to manually work out a trace for some very simple example.

However, all Z3 references seem to be how to code in it; or a very high level description of their algorithm. I am unable to find a description of the algorithms used. Is this information not made public by Microsoft?

Could anyone quote any references (papers/books) which give a comprehensive insight into Z3's theory + working?

Upvotes: 4

Views: 702

Answers (1)

alias
alias

Reputation: 30418

My personal opinion is that the best reference to start with is Kroening and Strichman's Decision Procedures book. (Make sure to get the 2nd edition as it has good updates!) It covers almost all topics of interest to certain depth, and has many references at the back for you to follow up on. The book also has a website http://www.decision-procedures.org with extra readings, slides, and project ideas.

Another book of interest in this field is Bradley and Manna's The Calculus of Computation. While this book isn't specific to SAT/SMT, it covers many of the similar topics and how these ideas play out in the realm of program verification. Also see http://theory.stanford.edu/~arbrad/pivc/index.html for the associated software/tools.

Of course neither of these books are specific to z3, so you won't find anything detailed about how z3 itself is constructed in them. For programming z3 and some of the theory behind it, the "tutorial" paper by Bjørner, de Moura, Nachmanson, and Wintersteiger is a great read.

Once you go through these, I suggest reading individual papers by the developers, depending on where your interests are:

And there's of course a plethora of resources on the internet, many papers, presentations, slide-decks etc. Feel free to ask specific questions directly in this forum, or for truly z3 internal specific questions, you can use their discussions forum.

Note Regarding the differences between editions of Kroening and Strichman's book, here’s what the authors have to say:

The first edition of this book was adopted as a textbook in courses worldwide. It was published in 2008 and the field now called SMT was then in its infancy, without the standard terminology and canonic algorithms it has now; this second edition reflects these changes. It brings forward the DPLL(T) framework. It also expands the SAT chapter with modern SAT heuristics, and includes a new section about incremental satisfiability, and the related Constraints Satisfaction Problem (CSP). The chapter about quantifiers was expanded with a new section about general quantification using E-matching and a section about Effectively Propositional Reasoning (EPR). The book also includes a new chapter on the application of SMT in industrial software engineering and in computational biology, coauthored by Nikolaj Bjørner and Leonardo de Moura, and Hillel Kugler, respectively.

Upvotes: 9

Related Questions