A SAT-Based Approach for Solving Suguru Puzzles: Theory and Experiment

Butrahandisya Butrahandisya; Muhammad Arzaki

doi:10.22342/jims.v32i2.1939

Butrahandisya Butrahandisya ⁽¹⁾ , Muhammad Arzaki ⁽²⁾

(1) Computing Laboratory, School of Computing, Telkom University, Indonesia,

(2) Computing Laboratory, School of Computing, Telkom University, Indonesia

https://doi.org/10.22342/jims.v32i2.1939

Issue
Vol. 32 No. 2 (2026): JUNE

Submitted
February 13, 2025

Accepted
November 25, 2025

Published
August 9, 2026

Keywords:

SAT encoding, SAT problems, SAT solver, Suguru puzzles

XML PDF

Abstract

We discuss a SAT-based approach for solving Suguru puzzles---one-player puzzles similar to Sudoku that were confirmed NP-complete in 2022. We first discuss the formal rules of the puzzles and provide a rigorous technique to translate such rules into propositional formulas in conjunctive normal form (CNF). The resulting formulas form what is called a SAT encoding, and we prove that the number of clauses and variables in our encoding is polynomially proportional to the puzzle's dimension. This encoding allows one to reduce Suguru puzzles to SAT problems, and we use this encoding to construct a declarative SAT-based program without any search algorithm in C++ for solving general Suguru puzzles. We perform experiments involving 230 test cases for Suguru instances of size n \times n where 6 \leq n \leq 15. Finally, we derive some empirical results from these experiments and argue that, in terms of running time, our SAT-based approach outperforms the previously proposed backtracking technique in solving larger puzzles.

Full text article

Generated from XML file

References

N. Inaba, Number block, http://inabapuzzle.com/honkaku/nblock.html, Accessed: 2023-06-19, Jul. 2001.

L. Robert, D. Miyahara, P. Lafourcade, L. Libralesso, and T. Mizuki, “Physical zero-knowledge proof and NP-completeness proof of Suguru puzzle,” Information and Computation, vol. 285, p. 104 858, 2022. https://doi.org/10.1016/j.ic.2021.104858.

C. Iwamoto and T. Ide, “Calculation Solitaire is NP-Complete,” IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, vol. 106, no. 3, pp. 328–332, 2023. https://doi.org/10.1587/transinf.2022fcl0002.

C. Iwamoto and T. Tokunaga, “Choco Banana is NP-complete,” IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, vol. 107, no. 9, pp. 1488–1491, 2024. https://doi.org/10.1587/transfun.2023dml0001.

C. Iwamoto and T. Ibusuki, “Polynomial-time reductions from 3SAT to Kurotto and Juosan puzzles,” IEICE Transactions on Information and Systems, vol. 103, no. 3, pp. 500–505, 2020. https://doi.org/10.1587/transinf.2019fcp0004.

J. Bosboom, E. D. Demaine, M. L. Demaine, A. Hesterberg, R. Kimball, and J. Kopinsky, “Path puzzles: Discrete tomography with a path constraint is hard,” Graphs and Combinatorics, vol. 36, no. 2, pp. 251–267, 2020. https://doi.org/10.1007/s00373-019-02092-5.

A. Adler, J. Bosboom, E. D. Demaine, M. L. Demaine, Q. C. Liu, and J. Lynch, “Tatamibari is NP-Complete,” in 10th International Conference on Fun with Algorithms (FUN 2021), M. Farach-Colton, G. Prencipe, and R. Uehara, Eds., ser. Leibniz International Proceedings in Informatics (LIPIcs), vol. 157, Dagstuhl, Germany: Schloss Dagstuhl–Leibniz-Zentrum f¨ur Informatik, 2020, 1:1–1:24, isbn: 978-3-95977-145-0. https://doi.org/10.4230/LIPIcs.FUN. 2021.1.

C. Iwamoto and T. Ide, “Five Cells and Tilepaint are NP-Complete,” IEICE Transcations on Information and Systems, vol. 105, no. 3, pp. 508–516, 2022. https://doi.org/10.1587/transinf.2021fcp0001.

E. D. Demaine, J. Lynch, M. Rudoy, and Y. Uno, “Yin-Yang Puzzles are NP-complete,” in 33rd Canadian Conference on Computational Geometry (CCCG) 2021, 2021.

S. Saha and E. D. Demaine, “ZHED is NP-complete,” in Proceedings of the 34th Canadian Conference on Computational Geometry (CCCG 2022), 2022.

E. C. Reinhard, M. Arzaki, and G. S. Wulandari, “Solving Tatamibari Puzzle Using Exhaustive Search Approach,” Indonesia Journal on Computing (IndoJC), vol. 7, no. 3, pp. 53–80, 2022.

M. I. Putra, M. Arzaki, and G. S. Wulandari, “Solving Yin-Yang Puzzles Using Exhaustive Search and Prune-and-Search Algorithms,” (IJCSAM) International Journal of Computing Science and Applied Mathematics, vol. 8, no. 2, pp. 52–65, 2022. https://doi.org/10.12962/j24775401.v8i2.13720.

M. T. Ammar, M. Arzaki, and G. S. Wulandari, “Note on Algorithmic Investigations of Juosan Puzzles,” Jurnal Ilmu Komputer dan Informasi, vol. 17, no. 1, pp. 19–35, 2024. https://doi.org/10.21609/jiki.v17i1.1184.

J. E. Sakti, M. Arzaki, and G. S. Wulandari, “A Backtracking Approach for Solving Path Puzzles,” Journal of Fundamental Mathematics and Applications (JFMA), vol. 6, no. 2, pp. 117–135, 2023. https://doi.org/10.14710/jfma.v6i2.18155.

B. Butrahandisya, M. Arzaki, and G. S. Wulandari, “Elementary Algorithmic Methods for Solving Suguru Puzzles,” (IJCSAM) International Journal of Computing Science and Applied Mathematics, vol. 10, no. 1, pp. 12–26, 2024. https://doi.org/10.12962/j24775401.v10i1.17249.

V. A. Fridolin, M. Arzaki, and G. S. Wulandari, “Elementary Search-based Algorithms for Solving Tilepaint Puzzles,” Indonesia Journal on Computing (Indo-JC), vol. 8, no. 2, pp. 36–64, 2023.

S. A. Cook, “The complexity of theorem-proving procedures,” in Proceedings of the third annual ACM symposium on Theory of computing, 1971, pp. 151–158. https://doi.org/10.7551/mitpress/12274.003.0036.

T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein, Introduction to algorithms, 4th Ed. MIT press, 2022.

R. M. Karp, “Reducibility among Combinatorial Problems,” in Complexity of Computer Computations: Proceedings of a symposium on the Complexity of Computer Computations, held March 20–22, 1972, at the IBM Thomas J. Watson Research Center, Yorktown Heights, New York, and sponsored by the Office of Naval Research, Mathematics Program, IBM World Trade Corporation, and the IBM Research Mathematical Sciences Department, R. E. Miller, J. W. Thatcher, and J. D. Bohlinger, Eds. Boston, MA: Springer US, 1972, pp. 85–103, isbn: 978-1-4684-2001-2. https://doi.org/10.1007/978-1-4684-2001-2_9.

M. Sipser, Introduction to the Theory of Computation, 3rd Edition. Cengage Learning, 2013.

H. A. Kautz, B. Selman, et al., “Planning as Satisfiability,” in ECAI, Citeseer, vol. 92, 1992, pp. 359–363.

C. Flanagan, R. Joshi, X. Ou, and J. B. Saxe, “Theorem proving using lazy proof explication,” in Computer Aided Verification: 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003. Proceedings 15, Springer, 2003, pp. 355–367. https://doi.org/10.1007/978-3-540-45069-6_34

A. Biere, M. Heule, and H. van Maaren, Handbook of satisfiability. IOS press, 2009, vol. 185.

A. Kuehlmann, V. Paruthi, F. Krohm, and M. K. Ganai, “Robust Boolean reasoning for equivalence checking and functional property verification,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 21, no. 12, pp. 1377–1394, 2002. https://doi.org/10.1109/tcad.2002.804386.

Z. Lei and S. Cai, “Solving (Weighted) Partial MaxSAT by Dynamic Local Search for SAT,” in IJCAI, vol. 7, 2018, pp. 1346–52. https://doi.org/10.24963/ijcai.2018/187.

T. Balyo, P. Sanders, and C. Sinz, “HordeSat: A massively parallel portfolio SAT solver,” in Theory and Applications of Satisfiability Testing–SAT 2015: 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings 18, Springer, 2015, pp. 156–172. https://doi.org/10.1007/978-3-319-24318-4_12.

P. Utomo and R. Pellikaan, “Binary puzzle as a SAT problem,” in Proceedings of the 2017 Symposium on Information Theory and Signal Processing, Benelux, 2017, pp. 223–229.

C. Ans´otegui, R. B´ejar, C. Fernandez, and C. Mateu, “Edge matching puzzles as hard SAT/CSP benchmarks (extended version),” Technical Report TR-1-08, Dept. of Computer Science, Universitat de Lleida, Tech. Rep., 2008.

A. M. Myat, K. K. Htwe, and N. Funabiki, “Fill-a-pix puzzle as a SAT problem,” in 2019 International Conference on Advanced Information Technologies (ICAIT), IEEE, 2019, pp. 244–249. https://doi.org/10.1109/aitc.2019.8920898.

M. T. Ammar, M. Arzaki, and G. S. Wulandari, “Efficient SAT-Based Approach for Solving Juosan Puzzles,” in International Conference on Mathematics: Pure, Applied and Computation, Springer, 2023, pp. 211–226. https://doi.org/10.1007/978-981-97-2136-8_16.

J. E. Sakti, M. Arzaki, and G. S. Wulandari, “Modeling Path Puzzles as SAT Problems and How to Solve Them,” in International Conference on Mathematics: Pure, Applied and Computation, Springer, 2023, pp. 227–245. https://doi.org/10.1007/978-981-97-2136-8_17.

L. Kolijn, “Generating and Solving Skyscrapers Puzzles Using a SAT Solver,” Bachelor Thesis, Radboud University, 2022.

I. Lynce and J. Ouaknine, “Sudoku as a SAT Problem,” in AI&M, 2006.

U. Pfeiffer, T. Karnagel, and G. Scheffler, “A Sudoku-Solver for Large Puzzles using SAT,” in LPAR short papers (Yogyakarta), 2010, pp. 52–57. https://doi.org/10.29007/79mc.

T. Weber, “A SAT-based Sudoku solver,” in LPAR, 2005, pp. 11–15.

C. Bright, J. Gerhard, I. Kotsireas, and V. Ganesh, “Effective problem solving using SAT solvers,” in Maple Conference, Springer, 2019, pp. 205–219. https://doi.org/10.1007/978-3-030-41258-6_15.

M. Ben-Ari, Mathematical Logic for Computer Science, 3rd Edition. Springer Science & Business Media, 2012. M. Huth and M. Ryan, Logic in Computer Science: Modelling and Reasoning about Systems, 2nd Edition. Cambridge university press, 2004.

T. D. Hansen, H. Kaplan, O. Zamir, and U. Zwick, “Faster k-sat algorithms using biased-PPSZ,” in Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing, 2019, pp. 578–589. https://doi.org/10.1145/3313276.3316359.

K. H. Rosen, Discrete Mathematics and Its Applications, 8th Ed. McGraw-Hill Higher Education, 2019, isbn: 0072424346.

S. H¨olldobler and V.-H. Nguyen, “An efficient encoding of the at-most-one constraint,” Technical Report 1304. Technische Universit¨aat Dresden, 2013.

M. Hoˇreˇnovsk´y, Modern SAT solvers: fast, neat and underused (part 3 of N ), https://codingnest.com/modern-sat-solvers-fast-neat-and-underused-part-3-of-n/, Accessed: 2023-5-22, Apr. 2019.

G. Audemard and L. Simon, “Predicting Learnt Clauses Quality in Modern SAT Solvers,” in IJCAI, vol. 9, 2009, pp. 399–404.

A. Biere, T. Faller, K. Fazekas, M. Fleury, N. Froleyks, and F. Pollitt, “CaDiCaL 2.0,” in International Conference on Computer Aided Verification, Springer, 2024, pp. 133–152.

A. Biere, K. Fazekas, M. Fleury, and M. Heisinger, “CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020,” in Proc. of SAT Competition 2020 – Solver and Benchmark Descriptions, T. Balyo, N. Froleyks, M. Heule, M. Iser, M. J¨arvisalo, and M. Suda, Eds., ser. Department of Computer Science Report Series B, vol. B-2020-1, University of Helsinki, 2020, pp. 51–53.

O. Janko, Suguru, https://www.janko.at/Raetsel/Suguru/index.htm, Accessed: 2022-10-11, Oct. 2022.

Authors

Butrahandisya Butrahandisya

Computing Laboratory, School of Computing, Telkom University

Muhammad Arzaki

Computing Laboratory, School of Computing, Telkom University

arzaki@telkomuniversity.ac.id (Primary Contact)

Butrahandisya, B., & Arzaki, M. (2026). A SAT-Based Approach for Solving Suguru Puzzles: Theory and Experiment. Journal of the Indonesian Mathematical Society, 32(2), 1939. https://doi.org/10.22342/jims.v32i2.1939

Download Citation

This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

Downloads

Download data is not yet available.

The resulting formulas form what is called a SAT encoding, and we prove that the number of clauses and variables in our encoding is polynomially proportional to the puzzle's dimension. This encoding allows one to reduce Suguru puzzles to SAT problems, and we use this encoding to construct a declarative SAT-based program without any search algorithm in C++ for solving general Suguru puzzles. We perform experiments involving 230 test cases for Suguru instances of size

1. Introduction

Single-player games that involve filling rectangular grids with numbers or symbols according to specific rules can be both challenging and captivating. Some of these games are inherently challenging and have a similar interesting property: finding solutions to these puzzles is typically “hard”, but once the solutions are found, checking whether these solutions satisfy the puzzles’ rules is relatively “easy”¹.A famous example of these puzzles Sis Sudoku. Another example is Suguru, a oneplayer game invented by Naoki Inaba, a prominent Japanese logic puzzle designer.

Suguru first emerged in 2001[1]and gained popularity in the theoretical computer science community in 2022 after Robert et al. proved its NP-completeness[2]. The puzzles are played in rectangular grids; a grid is partitioned into one or moreregions. Each region contains one or more orthogonally connected cells. Initially, some cells in the grid might be empty or filled with positive integers. These pre-filled cells are called thehint cellsor simplyhints. The objective of this puzzle is similar to the famous Sudoku—each empty cell must be filled with exactly one positive integer satisfying particular constraints. Suguru puzzles basically only have two rules: (1) for every region, each cell in that region must be filled with a unique integer between one and the number of cells in such a region, and (2) any two adjacent cells in the grid, either orthogonally or diagonally, must be filled with distinct integers.

Figure 1.An instance of a Suguru puzzle(Fig. 1a)and its solution(Fig. 1b).

Fig. 1illustrates an example of a Suguru puzzle instance and its solution. Here, we consider a Suguru puzzle of size \(6 × 6\). The instance inFig. 1aconsists of nine regions: there are six regions of size 5 and one region each of size 1, 2, and 3. The instance has seven hint cells. Notice that the solution to this instance inFig. 1bpreserves these hint cells.

The computational aspects of various one-player puzzles have attracted interest in the theoretical computer science community, especially in their connection to NP-complete problems. In the last six years, many single-player logic puzzles were proven NP-complete, such as Calculation Solitaire[3], Choco Banana[4], Juosan[5], Path Puzzles[6], Suguru[2], Tatamibari[7], Tilepaint[8], Yin-Yang[9], and ZHED[10]. Various techniques have been proposed to solve some of these NP-complete puzzles. Most of them consider imperative approaches, such as the exhaustive search for solving Tatamibari[11], the prune-and-search technique for solving Yin-Yang[12], as well as various backtracking approaches for solving Juosan[13], Path Puzzles[14], Suguru[15], and Tilepaint[16]. Typically, these algorithms involve sophisticated search-based criteria in their computational steps. One of them, namely the backtracking approach for solving Suguru puzzles explained in[15], exhibits a factorial upper bound for its running time complexity—which is not optimal for an NP-complete problem.

The Boolean satisfiability problem (SAT problem) is a fundamental problem in theoretical computer science and mathematical logic. It is the first established NP-complete problem[17],[18],[19],[20]. Theoretically, all NP-complete problems can be transformed into SAT problem instances. This property enables various NPcomplete problems to be solved by SAT solvers—algorithms specifically designed to determine the satisfiability of propositional formulas. Due to its versatility, SAT solvers have been used to assist various problems in computer science, such as automated planning and scheduling[21], automated theorem proving[22], formal software or hardware verification[23],[24], solving complex optimization problem[25], and various aspects of artificial intelligence[26].

Numerous studies have investigated SAT-based approaches for solving singleplayer logic puzzles, such as binary puzzles[27], edge matching puzzles[28], fill-a-pix[29], Juosan[30], Path Puzzles[31], Skyscraper[32], Sudoku[33],[34],[35], and other various single player puzzles[36]. A recent extensive investigation by Bright et al. demonstrates the efectiveness of the SAT-based approach in solving puzzles using the declarative approach[36]. In this approach, one focuses on describing the problems and their constraints as sets of Boolean formulas, rather than providing a sequence of imperative commands. Some empirical performance comparisons of the SAT-based and imperative search-based approaches for solving logic puzzles were recently discussed in[30],[31]. Ammar et al. showed that Juosan puzzles with up to 1350 cells can be solved in less than one second on a standard personal computer, significantly outperforming the backtracking approach, which required four days or more to solve the same puzzles on the same machine[30]. Sakti et al. showed that the SAT-based approach outperforms the backtracking algorithm for solving Path Puzzles if the number of cells is suficiently large[31]. Nevertheless, one should note that, in earlier studies, the imperative paradigms still outperformed the SAT-based ones for

.....

Read Counter : 87 Download : 114

Share Now

A SAT-Based Approach for Solving Suguru Puzzles: Theory and Experiment

Abstract

Full text article

References

Authors

Address

Contact Info

Article Sidebar

Abstract

Full text article

References

Authors

Article Details

Address

Contact Info