Hacker News Reader

Basically, it solves the problem of finding a setting of variables that is compatible with some set of constraints. This is NP-hard but Z3 is in practice very fast nonetheless.

A case study/glowing review from a programmer at Microsoft is here:

https://medium.com/@ahelwer/checking-firewall-equivalence-wi...

View on HN

You could be a little more precise and say that it's NP-complete. :-)

That actually depends on the logic being used. Some of the logics supported by Z3 are not even decidable. In fact, even solving quantifier-free bit-vector formulas is NEXPTIME-complete [0] when using a binary encoding.

[0] http://smt2012.loria.fr/paper7.pdf

Thanks for the clarification!

What do Z3 and other SMT solvers do if you ask them about undecidable questions? Do they potentially run forever?

Reply on news.ycombinator.com