If people are using this for interesting projects, I'd love some details.
http://bugchecker.net is a site that does automated testing (dynamic analysis). We use STP.
Z3: A high-performance theorem prover from Microsoft Research
41–50 of 50 posts
Re: Z3: A high-performance theorem prover from Microsoft Research
#42In terms of applicability, SMT (satisfiability module theory) solvers basically allow you to do things which are slightly more complex than plain SAT solving. If you're looking to learn more, Leonardo has a nice introduction to SMT and its applications over here: http://dl.acm.org/citation.cfm?id=1995394 . To make a long story short, various problems in program verification and static analysis have seen success with…
Pardon the relative ignorance... but I thought these types of problems (SAT and SMT) were NP-Complete in the general case? Does Z3 do something special (eg apply heuristics)? It looks very impressive!
http://www.csl.sri.com/users/rushby/slides/jaist07.pdf
See "SMT Solvers: Disruptive Innovation in Theorem Proving", Rushby, 2007.
> SAT solving is the quintessential NP-complete problem. But now amazingly fast in practice (most of the time)
> SMT ... generalizes SAT solving by adding the ability to handle arithmetic and other decidable theories
Re: Z3: A high-performance theorem prover from Microsoft Research
#43Earlier quoted context omitted.
"Commercial = I make money from using this; Non-commercial = NOT commercial " False. There are cases where commercial was held to mean "any use by a for profit company, regardless if the use is research, earns money directly or indirectly", etc.
Admittedly with a European viewpoint, either common law based (UK) or administrative law based (France, Belgium), there have been cases where commercial was held to mean has the company benefited in a tangible way from its use of such licenced software. Although if you speak to a lawyer I'm sure their training would immediately start highlighting this as a concern I don't believe it should be in the vast majority of…
I wonder what would happen here in Scotland - we don't have punitive damages so the most you can be awarded in court is the loss you can demonstrate to have suffered.
So if I use a software package commercially and don't pay for it perhaps the maximum I could be sued for in the local courts would be the license fee I didn't pay. If there is no "commercial" license then could it really be said that a loss has been suffered?
[NB I know contracts and licenses usually have clauses stating the jurisdiction where disputes will be resolved]
Re: Z3: A high-performance theorem prover from Microsoft Research
#44If people are using this for interesting projects, I'd love some details.
There's a stack of software verification projects, most probably using Z3, here - http://www.rise4fun.com/
Re: Z3: A high-performance theorem prover from Microsoft Research
#45If people are using this for interesting projects, I'd love some details.
The small project i'm developing for my Phd, "Symbolic Exploit Assistant" [1] (SEA) is using it.
Re: Z3: A high-performance theorem prover from Microsoft Research
#46In terms of applicability, SMT (satisfiability module theory) solvers basically allow you to do things which are slightly more complex than plain SAT solving. If you're looking to learn more, Leonardo has a nice introduction to SMT and its applications over here: http://dl.acm.org/citation.cfm?id=1995394 . To make a long story short, various problems in program verification and static analysis have seen success with…
Pardon the relative ignorance... but I thought these types of problems (SAT and SMT) were NP-Complete in the general case? Does Z3 do something special (eg apply heuristics)? It looks very impressive!
SAT is NP-complete, but there are certain properties that allow theorem provers to show that a particular instance is overconstrained (and therefore unsatisfiable), or underconstrained (and many solutions exist). It's at a particular point, so-called phase transitions, where one finds the very hard instances. As an example, when characterizing 3-SAT instances by grouping by their ratio of clauses to variables, the very hard instances are grouped around a value of ~4.3.
Re: Z3: A high-performance theorem prover from Microsoft Research
#47Earlier quoted context omitted.
Admittedly with a European viewpoint, either common law based (UK) or administrative law based (France, Belgium), there have been cases where commercial was held to mean has the company benefited in a tangible way from its use of such licenced software. Although if you speak to a lawyer I'm sure their training would immediately start highlighting this as a concern I don't believe it should be in the vast majority of…
I wonder what would happen here in Scotland - we don't have punitive damages so the most you can be awarded in court is the loss you can demonstrate to have suffered. So if I use a software package commercially and don't pay for it perhaps the maximum I could be sued for in the local courts would be the license fee I didn't pay. If there is no "commercial" license then could it really be said that a loss has been suf…
I suspect they would say that the commercial value of their solver, for which no publicly available license exists, is some very high dollar amount which they will offer to you as a courtesy.
Re: Z3: A high-performance theorem prover from Microsoft Research
#48If people are using this for interesting projects, I'd love some details.
Not about Z3 in particular, but a very interesting application of solvers:
This weblog talks about procedural content generation (PCG) for games: http://www.gamesbyangelina.org/
It's used in some roguelike games to make sure the procedurally generated levels/rooms are playable/winnable.
It's also used in puzzle games where constraints are set for a certain puzzle level to exhibit certain characteristics in the puzzle solution, but the puzzle itself is randomly generated according to these constraints.
There's a couple of articles about constraint solvers on that site, but I remember this one was most striking: http://www.gamesbyangelina.org/2013/06/the-saturday-paper-go...
Re: Z3: A high-performance theorem prover from Microsoft Research
#49Did anyone make a Javascript version of this with emscripten? I am currently using Z3 on the server side but would really like a client side solution to save computational resources.
The license is a non-commercial one, which makes it impractical for many use cases. Could be why it hasn't been ported yet (I might have done so myself, had the license been otherwise).
If you want to use it for commercial purposes, there is probably a way to get a license from them for that.
Re: Z3: A high-performance theorem prover from Microsoft Research
#50In terms of applicability, SMT (satisfiability module theory) solvers basically allow you to do things which are slightly more complex than plain SAT solving. If you're looking to learn more, Leonardo has a nice introduction to SMT and its applications over here: http://dl.acm.org/citation.cfm?id=1995394 . To make a long story short, various problems in program verification and static analysis have seen success with…
Pardon the relative ignorance... but I thought these types of problems (SAT and SMT) were NP-Complete in the general case? Does Z3 do something special (eg apply heuristics)? It looks very impressive!
Although SAT is indeed NP-complete, modern solvers are ridiculously fast for the kinds of SAT queries that appear in scenarios like hardware model checking and verification. It's not uncommon for queries with millions of variables and clauses to be solved in a matter of seconds. There are some algorithmic tricks combined with clever data structures and search space exploration heuristics that make this possible.
btw, if you're curious about the workings of a modern SAT solver, the first few sections of this paper: http://www.georg.weissenbacher.name/papers/mod12.pdf should make interesting and hopefully accessible reading.
Unfortunately, I don't know enough about the internals of Z3 to know what specifically makes it the fastest SMT solver. But I also don't think it's too far wrong to say that SMT solvers like Z3 are fast because the underlying SAT solver they use is very fast.