[harperlee]

Could please someone informed explain how is this more restricted to only prove theorems, instead of being a more general prolog-like system?

From the Microsoft Research page, I read:

> Z3 is a high-performance theorem prover being developed at Microsoft Research. Z3 supports linear real and integer arithmetic, fixed-size bit-vectors, extensional arrays, uninterpreted functions, and quantifiers. Z3 is integrated with a number of program analysis, testing, and verification tools from Microsoft Research.

And with my current knowledge (which is low on the matter) I can't reconcile arithmetic, arrays, quantifiers, etc. with general program verification...

[eslaught]

Z3 is an SMT solver (https://en.wikipedia.org/wiki/Satisfiability_modulo_theories). You can think of it like a SAT solver with extra optimizations for certain domains, so that it doesn't need to do bit-blasting to e.g. compare integers. SMT is NP-complete, just like SAT, but it is decidable (so the solver will "eventually" give you a yes/no answer, though "eventually" could be a long time).

This is in pretty stark contrast to Prolog, which includes features which make it undecidable. Therefore you can make Prolog loop infinitely, while that is not possible in an SMT solver.

[mjn]

Fwiw some of the later logic-programming work coming out of Prolog has produced languages with Prolog-like syntax but without statement order being significant, and guaranteed termination. This paradigm, Answer Set Programming (ASP), is also based on solvers, so has some relationship to SMT, but feels more like Prolog to program, e.g. it has negation-as-failure. My favorite implementation is from the University of Potsdam [1].

Imo it's a much nicer modeling language, especially for incremental formalization, in part because of implementing a nonmonotonic rather than classical logic. It also has a nice generative-programming style where you can define generative spaces via "choice rules", where the solver is explicitly given a free choice for some variables, subject to constraints, and returns a satisfying artifact/model. That allows using it to construct constrained generative systems (e.g. generative music [2], level generation [3]). But Z3 far outperforms ASP solvers on problems where variables range over large domains (like "32-bit integer") because of the MT part of SMT. There's some experimental work on trying to combine the approaches, using Z3 (or another SMT solver) as the solver backend for a logic-programming system [4], but I don't know how usable it is.

[1] http://potassco.sourceforge.net/

[2] http://arxiv.org/abs/1006.4948

[3] http://pcgbook.com/wp-content/uploads/chapter08.pdf

[4] http://peace.eas.asu.edu/joolee/papers/aspmt-system-jelia.pd...

[NotableAlamode]

I'm not sure I'd set up an opposition between SAT solvers like Z3 on one hand, and ASP on the other. I recommend to think of ASP (and other approaches like CSP (constraint satisfaction problems)) as high-level languages for solving combinatorial problems.

In this understanding, high-level (ASP, CSP) contrasts with low-level (SAT and SMT) for the same problem domain: just as with high- and low-level programming languages like Java are compiled down to low-level programming languages like x86 machine code, high-level formalism like ASP, CSP, ... can be compiled down to low-level SAT/SMT.

SAT/SMT is the assembly language of combinatorial problems because you have to state explicitly all forbidden solutions using CNF (conjuncive normal form). For examle if you have variables x, y and z, then the CNF ( x \/ y \/ not z ) /\ ( not x /\ not y ) has as models all maps from {x, y, z} to {0, 1} except {x=0, y=0, z=1}, {x=1, y=1, z=1} and {x=1, y=1, z=0}. The problem with using CNFs to enumerate forbidden solutions is that the formulae can be long (just like assembler programs can be long). With high-level formalisms like ASP you often get a much more succinct specification.

With a bit of squinting, you can even see first-order logic as a high-level formalism that compiles down to propositional logic (via skolemisation, resolution, unification, herbrand etc).

[mjn]

In some theoretical sense I agree with that view, but I don't think we're currently at that stage from a practical perspective. Today, the established ASP solvers have performance and expressivity tradeoffs relative to the established SMT solvers. There are some early experiments (like the one I linked) that aim to do things like use SMT solvers as an ASP backend, but they are very much research stage. And they are also (so far) a bit "messy", requiring source-level changes in order to take advantage of Z3, rather than being able to transparently "compile" general ASP programs to take advantage of efficient solvers.

[NotableAlamode]

Intersting. I did not consider the question from a practical POV. What are the main technical impediments with using SMT solvers are ASP backends?

[poizan42]

Uhm you can throw diophantine equations after Z3 which certainly isn't a decideable problem. I have no idea whether it errs on the side of termination (i.e. not giving an answer) or non-termination (i.e. running forever).

[deckar01]

The very first example on Github show that checking a conjecture results in one of 3 outcomes:

- Unsatisfied (unsat)

- Satisified (sat)

- Unknown (unknown)

[darkmighty]

He just stated non-termination is not an option, therefore...

[ulber]

Not all theory fragments supported by Z3 are decidable: Z3 includes an incomplete decision procedure for non-linear real arithmetic [1].

[1] http://stackoverflow.com/a/13898524

[ufo]

It might be better to see Ze and other SMT solvers as souped up SAT solvers instead of comparing them to general theorem provers.

The neat thing about Z3 is that it has efficient solvers for the more specific subproblems (linear programming, bit vectors, etc) that you can't have if you state everything using "general" constraint programming. At the same time, Z3 lets you work at a higher level of abstraction - for example, you can reason about bit verctors or arithmetic directly instead of having to encode it with boolean formulas.

[richdougherty]

Z3 has a core engine optimised to solve certain types of problems. To use Z3 for higher-level problems, such as program verification, you first translate your higher-level problems into problems that Z3 understands. Z3 might not be suitable for all problems, but it is meant to be highly optimised for the problems that it can handle.

http://research.microsoft.com/en-us/um/redmond/projects/z3/z... http://research.microsoft.com/en-us/um/people/leonardo/files... http://research.microsoft.com/en-us/events/z3dtu/dtu-jan4-z3...