A SAT-based parser and completer for pictures specified by tiling

摘要

Pictures or patterns have been formally specified by different methods such as grammars. An alternative approach is based on tiling systems (TS) (Wang tiles are an analogous and equivalent formalism), whereby the picture is obtained by first covering it with a specified set of 2×2 tiles, then by performing a pixel by pixel mapping. TS are a powerful technique: the corresponding pictures can be recognized by non-deterministic cellular automata, which are more powerful than the four-ways automata. The difficulty to write such specifications for non-elementary pictures, and the NP-complete computational complexity of TS picture recognition have so far blocked any attempt to application. We have implemented a recognizer and generator for TS pictures in a very attractive, unconventional way, by transforming the tiling problem into a SAT (Boolean satisfiability) one, then using an efficient off-the-shelf SAT-solver. The prototype is fast enough to experiment on reasonably sized samples, and has the bonus of being able to complete or extrapolate a partial or noisy picture. The tool is invaluable to assist in writing picture specification. A series of examples shows how to specify patterns using TS.