Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

The Z3 theorem prover is now open source

research.microsoft.com

Post reply on HN
Print view View original

51–60 of 77 posts

Re: The Z3 theorem prover is now open source

#51

Post by Dn_Ab »

wiradikusuma wrote: post #15
ot wrote: post #4

This is great news! When I was at MSR I heard the rumor that they wanted to sell Z3, not open-source it! Some context, as not everybody may have heard about it. Z3 is an SMT [1] solver. Since SMT generalizes SAT, it is clearly NP-hard, so a number of heuristics are needed. In particular, Z3 won several SMT speed competitions, so it has been for long the fastest SMT solver. You can play with it online using its Lisp-l…

what is the practical uses of this (or SMT in general)? i've read the referenced Wikipedia but still don't understand.

I have only made light contact with SMTs in my explorations but SMT solvers have massive applicability. They're used in theorem proving - verification, dependent typing, contracts - scheduling, planning, and for understanding/modelling cell regulatory networks in biology.

Satisfiability stuff is interesting because it shows that just because something is NP-complete doesn't mean that it is unapproachable or 'hard' (just as linear programming shows just cause something is in P doesn't mean it is 'easy' - for large values of easy). To ground the concept you can roughly categorize it with logic programming, answer set programming, constraint satisfaction and integer programming. I've made use of answer set programming for certain planning problems as a kind of better prolog but SMT is a 'bit' more flexible.

Re: The Z3 theorem prover is now open source

#52

Post by tluyben2 »

That's excellent (good to learn from, shame it's only non commercial; it's a step forward though)! I was accidentally checking rise4fun for open source just last week. I hope they open source more; unfortunately the project I'm most curious about at the moment (quickcode) will not be open sourced as it is officially part of Excel now.

Re: The Z3 theorem prover is now open source

#53

Post by mjn »

Dn_Ab wrote: post #51
wiradikusuma wrote: post #15

Earlier quoted context omitted.

what is the practical uses of this (or SMT in general)? i've read the referenced Wikipedia but still don't understand.

I have only made light contact with SMTs in my explorations but SMT solvers have massive applicability. They're used in theorem proving - verification, dependent typing, contracts - scheduling, planning, and for understanding/modelling cell regulatory networks in biology. Satisfiability stuff is interesting because it shows that just because something is NP-complete doesn't mean that it is unapproachable or 'hard' (j…

> I've made use of answer set programming for certain planning problems as a kind of better prolog but SMT is a 'bit' more flexible.

I suppose it depends on what you mean by flexible. I would say that ASP is more flexible as a modeling language—you can specify all sorts of logic and constraints in it in a fairly expressive logical formalism, with both generative (Prolog-like) and constraint-oriented (CSP-like) language constructs. Particularly with the extensions the Potassco people have been making in their version: http://potassco.sourceforge.net/

However, current ASP solvers ground to variable-free (propositional) programs before solving, which means they blow up on large-ish integer domains, since you end up propositionalizing the whole integer range. I've had some examples where just grounding out the problem takes ages, but then it's nearly instant to solve once the grounding is done. SMT avoids that by providing a way to ground "modulo" a domain theory, rather than fully grounding, with a theory of integers being a common example.

Re: The Z3 theorem prover is now open source

#54

Post by tikhonj »

wiradikusuma wrote: post #15
ot wrote: post #4

This is great news! When I was at MSR I heard the rumor that they wanted to sell Z3, not open-source it! Some context, as not everybody may have heard about it. Z3 is an SMT [1] solver. Since SMT generalizes SAT, it is clearly NP-hard, so a number of heuristics are needed. In particular, Z3 won several SMT speed competitions, so it has been for long the fastest SMT solver. You can play with it online using its Lisp-l…

what is the practical uses of this (or SMT in general)? i've read the referenced Wikipedia but still don't understand.

They can be used for program synthesis. That is, given some high-level specification, you can use an SMT solver to generate code fitting that specification. You can also use them to verify that some code does fit a specification and, if it doesn't, to find the part of the code causing the actual problem (the minimal unsat core).

A particular example would be to take some existing code with holes (just parts left out) and some assertions about the code's behavior, encode both as logic formulas and try to find a satisfying assignment for the holes. When you have a possible assignment, you can verify it with the same encoding. You can then use the satisfying assignment to fill in the holes in the initial program, which are ideally very tedious to code by hand.

Re: The Z3 theorem prover is now open source

#55

Post by wolfgke »

raphinou wrote: post #27
wiradikusuma wrote: post #15

Earlier quoted context omitted.

what is the practical uses of this (or SMT in general)? i've read the referenced Wikipedia but still don't understand.

another example: package dependencies resolution on Linux distributions.

This can far more easily be done by topological sorting.

Re: The Z3 theorem prover is now open source

#58

Post by zvrba »

People bitching about MS misusing the term "open-source" are, IMO, ungrateful SOBs who have never attempted to implement a non-trivial algorithm based on nothing but a stack of academic papers.

For me, the greatest value in having the source is to learn from it, not to hijack it.

Re: The Z3 theorem prover is now open source

#59

Post by ac »

wiradikusuma wrote: post #15
ot wrote: post #4

This is great news! When I was at MSR I heard the rumor that they wanted to sell Z3, not open-source it! Some context, as not everybody may have heard about it. Z3 is an SMT [1] solver. Since SMT generalizes SAT, it is clearly NP-hard, so a number of heuristics are needed. In particular, Z3 won several SMT speed competitions, so it has been for long the fastest SMT solver. You can play with it online using its Lisp-l…

what is the practical uses of this (or SMT in general)? i've read the referenced Wikipedia but still don't understand.

Various forms of program analysis/verification. Some examples of applications where SMT is heavily used are automated theorem provers, symbolic execution engines, model checking tools.

Re: The Z3 theorem prover is now open source

#60

Post by algorias »

zvrba wrote: post #58

People bitching about MS misusing the term "open-source" are, IMO, ungrateful SOBs who have never attempted to implement a non-trivial algorithm based on nothing but a stack of academic papers. For me, the greatest value in having the source is to learn from it, not to hijack it.

I think a lot of people appreciate the move MS made while simultaneously condemning them for their casual appropriation of a term having a well-established meaning. They've updated the blog post in the meantime, so this is a non-issue.

Resorting to ad-hominems does nothing to strengthen your argument, btw.

Post reply on HN