SAT-Based Analysis of Cellular Automata

Abstract. Cellular Automata are a powerful formal model for describing physical and computational processes. Qualitative analysis of Cellular Automata is in general a hard problem. In this paper we will investigate the applicability of modern SAT solvers to this problem. For this purpose we will define an encoding of reachability problems for Cellular Automata into SAT. The encoding is built in a modular way and can be used to test inverse reachability problems in a natural way. In the paper we will present experimental results obtained using the SAT-solver zChaff.

• Type: Conference
• Year: 2004
• Where: ACRI
• Authors: Massimo D'Antonio, Giorgio Delzanno
• Keywords: ACRI 2004, Cellular Automata, Powerful Formal Model, Reachability Problems