Games became popular, within the formal verification community, after their application to automatic synthesis of circuits from specifications, and they have been receiving more and more attention since then. This paper focuses on coding the “Sokoban” puzzle, i.e., a very complex single-player strategy game. We show how its solution can be encoded and represented as a Bounded Model Checking problem, and then solved with a SAT solver. After that, to cope with very complex instances of the game, we propose two different ad-hoc divide-and-conquer strategies. Those strategies, somehow similar to state-of-the-art abstraction-and-refinement schemes, are able to decompose deep Bounded Model Checking instances into easier subtasks, trading-off between efficiency and completeness. We analyze a vast set of difficult hard-to-solve benchmark games, trying to push forward the applicability of state-of-the-art SAT solvers in the field. Those results show that games may provide one of the next frontier for the SAT community.
Back to Basics: Solving Games with SAT / Quer, Stefano. - In: ADVANCES IN ELECTRICAL AND COMPUTER ENGINEERING. - ISSN 1582-7445. - STAMPA. - 16:3(2016), pp. 91-98. [10.4316/AECE.2016.03013]
Back to Basics: Solving Games with SAT
QUER, Stefano
2016
Abstract
Games became popular, within the formal verification community, after their application to automatic synthesis of circuits from specifications, and they have been receiving more and more attention since then. This paper focuses on coding the “Sokoban” puzzle, i.e., a very complex single-player strategy game. We show how its solution can be encoded and represented as a Bounded Model Checking problem, and then solved with a SAT solver. After that, to cope with very complex instances of the game, we propose two different ad-hoc divide-and-conquer strategies. Those strategies, somehow similar to state-of-the-art abstraction-and-refinement schemes, are able to decompose deep Bounded Model Checking instances into easier subtasks, trading-off between efficiency and completeness. We analyze a vast set of difficult hard-to-solve benchmark games, trying to push forward the applicability of state-of-the-art SAT solvers in the field. Those results show that games may provide one of the next frontier for the SAT community.Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
https://hdl.handle.net/11583/2648265
Attenzione
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo