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

Solution 1:

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:

• Bjørner: https://www.microsoft.com/en-us/research/people/nbjorner/publications/

• de Moura: https://www.microsoft.com/en-us/research/people/leonardo/publications/

• Wintersteiger: https://www.microsoft.com/en-us/research/people/cwinter/publications/

• Nachmanson: https://www.microsoft.com/en-us/research/people/levnach/publications/

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.