6 ms·

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 Microsof

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...

ufo 12y ago
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.
eslaught 12y ago
Z3 is an SMT solver (https://en.wikipedia.org/wiki/Satisfiability_modulo_theories 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.
- poizan42 12y ago
  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 12y ago
    The very first example on Github show that checking a conjecture results in one of 3 outcomes: - Unsatisfied (unsat) - Satisified (sat) - Unknown (unknown)
  - darkmighty 12y ago
    He just stated non-termination is not an option, therefore...
- ulber 12y ago
  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 http://stackoverflow.com/a/13898524
- mjn 12y ago
  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/ http://potassco.sourceforge.net/ [2] http://arxiv.org/abs/1006.4948 http://arxiv.org/abs/1006.4948 [3] http://pcgbook.com/wp-content/uploads/chapter08.pdf http://pcgbook.com/wp-content/uploads/chapter08.pdf [4] http://peace.eas.asu.edu/joolee/papers/aspmt-system-jelia.pdf http://peace.eas.asu.edu/joolee/papers/aspmt-system-jelia.pd...
  - NotableAlamode 12y ago
    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).
richdougherty 12y ago
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/z3.pdf http://research.microsoft.com/en-us/um/redmond/projects/z3/z... http://research.microsoft.com/en-us/um/people/leonardo/files/cfv09.pdf http://research.microsoft.com/en-us/um/people/leonardo/files... http://research.microsoft.com/en-us/events/z3dtu/dtu-jan4-z3.pdf http://research.microsoft.com/en-us/events/z3dtu/dtu-jan4-z3...

ufo 12y ago

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.

eslaught 12y ago

Z3 is an SMT solver (https://en.wikipedia.org/wiki/Satisfiability_modulo_theories 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.

poizan42 12y ago
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 12y ago
  The very first example on Github show that checking a conjecture results in one of 3 outcomes: - Unsatisfied (unsat) - Satisified (sat) - Unknown (unknown)
- darkmighty 12y ago
  He just stated non-termination is not an option, therefore...
ulber 12y ago
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 http://stackoverflow.com/a/13898524
mjn 12y ago
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/ http://potassco.sourceforge.net/ [2] http://arxiv.org/abs/1006.4948 http://arxiv.org/abs/1006.4948 [3] http://pcgbook.com/wp-content/uploads/chapter08.pdf http://pcgbook.com/wp-content/uploads/chapter08.pdf [4] http://peace.eas.asu.edu/joolee/papers/aspmt-system-jelia.pdf http://peace.eas.asu.edu/joolee/papers/aspmt-system-jelia.pd...
- NotableAlamode 12y ago
  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).

richdougherty 12y ago

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/z3.pdf http://research.microsoft.com/en-us/um/redmond/projects/z3/z... http://research.microsoft.com/en-us/um/people/leonardo/files/cfv09.pdf http://research.microsoft.com/en-us/um/people/leonardo/files... http://research.microsoft.com/en-us/events/z3dtu/dtu-jan4-z3.pdf http://research.microsoft.com/en-us/events/z3dtu/dtu-jan4-z3...