Automatically Solving Deduction Games via Symbolic Execution, Model Counting, and Entropy Maximization

Mara Downing, Chris Thompson and Professor Lucas Bang had their paper titled “Automatically Solving Deduction Games via Symbolic Execution, Model Counting, and Entropy Maximization” accepted at the AAAI Conference on Artificial Intelligence and Interactive Digital Entertainment Strategy Game Workshop. Mara and Chris designed a DSL for expressing a class of puzzles called “deduction games,” implemented a symbolic execution engine for it using an automated theorem prover, and then wrote and entropy maximizer that outputs the steps of game solution. The main takeaway is that you can give their system the source code of a game and it will then automatically solve the game, playing it in real time.