We at Radix Labs (S18) use Z3 (and CVC4/SyGuS) heavily as a library to solve place-and-route problems for goal directed robot path planning problems. Its facil

We at Radix Labs (S18) use Z3 (and CVC4/SyGuS) heavily as a library to solve place-and-route problems for goal directed robot path planning problems. Its facilities for program construction over the integers, sets, bitvectors, and reals make it an ideal candidate for this, especially when leveraging nu-Z3 for optimization over these. With Z3, we’re able to construct optimized routes for robots extremely fast (especially with extensions over the techniques described in [1]), and as a direct result, derive value for our customers as execution time is important when dealing with expensive equipment. A couple of my friends over at trail of bits do the work that saurabh does at synthetic minds, and their code is open source so you can take a look at it. [2] It’s a decently active field of research, with solvers trading blows in the annual SMT-COMP [3]. check out their instances to see how people really use them. [1] https://papers.nips.cc/paper/8233-learning-to-solve-smt-formulas.pdf https://papers.nips.cc/paper/8233-learning-to-solve-smt-form... [2] https://www.trailofbits.com/services/blockchain-security/ https://www.trailofbits.com/services/blockchain-security/ [3] http://smtcomp.sourceforge.net/2018/ http://smtcomp.sourceforge.net/2018/