3 ms·
Can I get a lam ns example of what z3 is and what it is?
by jaunkst 8y ago
Can I get a lam ns example of what z3 is and what it is?
- currymj 8y agoBasically, 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-with-z3-c2efe5051c8f https://medium.com/@ahelwer/checking-firewall-equivalence-wi...
- schoen 8y agoYou could be a little more precise and say that it's NP-complete. :-)
- OxO4 8y agoThat 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 http://smt2012.loria.fr/paper7.pdf
- schoen 8y agoThanks for the clarification! What do Z3 and other SMT solvers do if you ask them about undecidable questions? Do they potentially run forever?
- patsplat 8y agoFound these links helpful: https://en.m.wikipedia.org/wiki/Satisfiability_modulo_theories#Applications https://en.m.wikipedia.org/wiki/Satisfiability_modulo_theori... https://github.com/Z3Prover/z3/wiki/Slides https://github.com/Z3Prover/z3/wiki/Slides Appears to be useful for static analysis and verification of a program.