Off topic but does anyone know if there is anywhere to learn about using formal methods to check board game rules? I've played a few games like Wherewolf (not the one-night variant) where I am intuitively sure at a certain number of players with certain rules the game is solved but would love to double check.
- if the problem is small enough, you could run an exhaustive search of options - in that case it really doesn't matter how you encode the rules, it could be any function returning a bool
- if you're trying to prove some invariant about the game, look at languages like Coq - they should help you
Fwiw, it’s a social deduction game where each role gains info or has an ability and each night they vote to kill someone and the wherewolfs kill someone. The game ends when the wherewolfs are dead or when they equal the number of villagers left alive. I’m pretty sure at a certain number of players regardless of roles if the villagers act in a certain way they win regardless of input from the wherewolves.
