Catan is a wonderful boardgame about strategy and chance. However, the chances of the game can become extremely skewed based on the board layout, which is typically decided randomly. This post describes how we can tackle this, and implements a tool (available online) to generate balanced boards using the IDP-Z3 reasoning engine, based on First Order Logic. Image from the Wikimedia Commons. Catan boards and balance Lets first get into what constitutes a Catan board. As shown in the image above...