Not about Z3 in particular, but a very interesting application of solvers: This weblog talks about procedural content generation (PCG) for games: http://www.ga

Not about Z3 in particular, but a very interesting application of solvers: This weblog talks about procedural content generation (PCG) for games: http://www.gamesbyangelina.org/ http://www.gamesbyangelina.org/ It's used in some roguelike games to make sure the procedurally generated levels/rooms are playable/winnable. It's also used in puzzle games where constraints are set for a certain puzzle level to exhibit certain characteristics in the puzzle solution, but the puzzle itself is randomly generated according to these constraints. There's a couple of articles about constraint solvers on that site, but I remember this one was most striking: http://www.gamesbyangelina.org/2013/06/the-saturday-paper-goldilocks-and-the-three-puzzles/ http://www.gamesbyangelina.org/2013/06/the-saturday-paper-go...