Here [1] is a cool project that uses Z3 to make graphics specified by constraints. I remember reading an article about someone using Z3 to optimize the placeme

Here [1] is a cool project that uses Z3 to make graphics specified by constraints. I remember reading an article about someone using Z3 to optimize the placement of cutout drawings on a piece of paper (kind of like a spritesheet) and optimizing for the smallest possible area in order to reduce the use of paper/materials. However, I can't seem to find the article anywhere. One more use of z3 is as one of the available solvers for a tool called gnatprove [2], which is used to prove/verify the correctness of programs written in the SPARK subset of the Ada programming language. SPARK is used to program safety-critical aeronautical/military projects. [1] https://www.anishathalye.com/2019/12/12/constraint-based-graphic-design/ https://www.anishathalye.com/2019/12/12/constraint-based-gra... [2] https://docs.adacore.com/spark2014-docs/html/ug/en/gnatprove.html https://docs.adacore.com/spark2014-docs/html/ug/en/gnatprove...