Solving Hitori puzzles using Satisfiablity Modulo Theories
R.J. Rietdijk (TU Delft - Electrical Engineering, Mathematics and Computer Science)
A.L.D. Latour – Mentor (TU Delft - Algorithmics)
T.J. Coopmans – Mentor (TU Delft - QCD/Coopmans Group)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
Modelling-and-solving paradigms are widely used to solve combinatorial problems, but comparisons of these paradigms on identical problem instances remain scarce and are often incomplete or biased. As a results, finding the correct paradigm for a given logic problem can be difficult. In this study, we evaluate the performance of the Satisfiability Modulo Theories (SMT) paradigm for solving Hitori puzzles, as part of a larger effort to compare modelling-and-solving paradigms. During the evaluation, the running time of the solver will be used as the primary performance statistic. Across all evaluated encodings, a straightforward encoding using linear integer arithmetic shows the best and most stable performance. Alternative encodings and redundant constraints generally do not improve performance, often increasing encoding size or adding unnecessary complexity. Results show that solver runtime is dominated by puzzle size and encoding size, with puzzle structure having little influence. These findings show that SMT is a suitable paradigm for solving Hitori puzzles, as the rules naturally translate into a compact encoding without the need for added complexity or redundancy.