[Cieplak]

I wonder if it uses Z3 under the hood for solving constraints. Very nice of MSFT to MIT license Z3. It's super useful for problems that result in circular dependencies when modeled in Excel, and require iterative solvers (e.g., goal seek). I use the python bindings, but unfortunately it's not as simple as `pip install` and requires a lengthy build/compilation. Well worth the effort, though.

https://github.com/Z3Prover/z3

https://github.com/Z3Prover/z3/issues/288

[tonmoy]

Love Z3. It is easy to use and very decent performance! I don't think MS is using Z3 on this product though, looks more like the smart enumeration based program synthesis

[c-cube]

I think most of the enumeration-based synthesis tools rely on a SMT solver (Z3 or CVC4, say) to learn from bad solutions.