Strategy Synthesis for General Deductive Games Based on SAT Solving

TL;DR

This paper introduces a flexible framework for modeling and solving deductive games using SAT solving, demonstrated through the Cobra tool to generate new insights into existing games.

Contribution

It presents a novel general framework for deductive games and implements it in a software tool, enabling new analysis and solution strategies.

Findings

Successfully modeled various deductive games

Generated new results for existing games

Demonstrated effectiveness of SAT-based approach

Abstract

We propose a general framework for modelling and solving deductive games, where one player selects a secret code and the other player strives to discover this code using a minimal number of allowed experiments that reveal some partial information about the code. The framework is implemented in a software tool Cobra, and its functionality is demonstrated by producing new results about existing deductive games.