Top

Published in:

2024 | OriginalPaper | Chapter

Efficient SAT-Based Approach for Solving Juosan Puzzles

Authors : Muhammad Tsaqif Ammar, Muhammad Arzaki, Gia Septiana Wulandari

Published in: Applied and Computational Mathematics

Publisher: Springer Nature Singapore

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Juosan is a single-player paper-and-pencil puzzle introduced in 2014 and shown to be NP-complete in 2018. This NP-completeness implies that the Juosan puzzle is polynomial-time reducible to the Boolean satisfiability (SAT) problem, thereby allowing us to transform the puzzle into SAT problems. This paper introduces an efficient SAT-based approach for solving the Juosan puzzles. We first discuss the rules and derived properties of Juosan puzzles and translate them into Boolean formulas in Conjunctive Normal Forms (CNF). We show that the number of clauses and propositional variables used in the encoding is polynomially proportional to the puzzle’s size. Using this encoding, we successfully implement a declarative program with no search algorithm using MiniSAT in C++ to solve any Juosan puzzle with up to \(1350\) cells in less than one second on a standard personal computer. Experimental results show that our SAT-based approach outperforms the optimized backtracking algorithm for larger puzzles.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Dynamic Response of Floating Crane During Lifting Operation: A Parametric Study

next chapter Modeling Path Puzzles as SAT Problems and How to Solve Them

Two Boolean formulas \(\phi \) and \(\psi \) are equisatisfiable if and only if the satisfiability of \(\phi \) implies the satisfiability of \(\psi \), and conversely.

Hearn, R.A., Demaine, E.D.: Games, Puzzles, and Computation. CRC Press (2009)

Lynce, I., Ouaknine, J.: Sudoku as a SAT Problem. In: AI &M (2006)

Kwon, G., Jain, H.: Optimized CNF encoding for sudoku puzzles. In: Proceedings of the 13th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR2006), pp. 1–5 (2006)

Henz, M., Truong, H.M.: Sudokusat-a tool for analyzing difficult sudoku puzzles. In: Tools and Applications with Artificial Intelligence, pp. 25–35 (2009)

Pfeiffer, U., Karnagel, T., Scheffler, G.: A Sudoku-solver for large puzzles using SAT. In: LPAR Short Papers (Yogyakarta), pp. 52–57 (2010)

Bright, C., Gerhard, J., Kotsireas, I., Ganesh, V.: Effective problem solving using SAT solvers. In: Maple Conference, pp. 205–219. Springer (2019)

Ansótegui, C., Béjar, R., Fernàndez, C., Mateu, C.: Edge matching puzzles as hard SAT/CSP benchmarks. In: Principles and Practice of Constraint Programming: 14th International Conference, CP 2008, Sydney, Australia, 14–18 September 2008. Proceedings of vol. 14, pp. 560–565. Springer (2008)

Chen, J.: Solving Rubik’s cube using SAT solvers (2011). Preprint at arXiv:1105.1436

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

10.

Myat, A.M., Htwe, K.K., Funabiki, N.: Fill-a-pix puzzle as a SAT problem. In: 2019 International Conference on Advanced Information Technologies (ICAIT), pp. 244–249. IEEE (2019)

11.

Kolijn, L.: Generating and solving skyscrapers puzzles using a SAT solver. Bachelor thesis, Radboud University (2022)

12.

Biere, A., Heule, M., van Maaren, H.: Handbook of Satisfiability, vol. 185. IOS Press (2009)

13.

Heule, M.J., Kullmann, O., Marek, V.W.: Solving very hard problems: cube-and-conquer, a hybrid SAT solving method. In: IJCAI, vol. 17, pp. 228–245 (2017)

14.

Bright, C., Kotsireas, I., Ganesh, V.: A SAT+ CAS method for enumerating Williamson matrices of even order. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 32 (2018)

15.

Iwamoto, C., Ibusuki, T.: Kurotto and Juosan are NP-complete. In: The 21st Japan Conference on Discrete and Computational Geometry, Graphs, and Games (JCDCG3 2018), pp. 46–48 (2018). https://link.springer.com/chapter/10.1007/978-3-030-90048-9_14

16.

Iwamoto, C., Ibusuki, T.: Polynomial-time reductions from 3SAT to Kurotto and Juosan puzzles. IEICE Trans. Inf. Syst. 103(3), 500–505 (2020). https://www.jstage.jst.go.jp/article/transinf/E103.D/3/E103.D_2019FCP0004/_pdf

17.

Iwamoto, C., Ide, T.: Moon-or-Sun, Nagareru, and Nurimeizu are NP-complete. IEICE Trans. Fundam. Electron. Commun. Comput. Sci., 1187–1194 (2022). https://www.jstage.jst.go.jp/article/transfun/advpub/0/advpub_2021DMP0006/_article/-char/ja/

18.

Robert, L., Miyahara, D., Lafourcade, P., Libralesso, L., Mizuki, T.: Physical zero-knowledge proof and NP-completeness proof of Suguru puzzle. Inf. Comput. 285, 104858 (2022). https://www.sciencedirect.com/science/article/pii/S0890540121001905

19.

Adler, A., Bosboom, J., Demaine, E.D., Demaine, M.L., Liu, Q.C., Lynch, J.: Tatamibari is NP-complete. In: Farach-Colton, M., Prencipe, G., Uehara, R. (eds.) 10th International Conference on Fun with Algorithms (FUN 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol. 157, pp. 1:1–1:24. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2020). https://drops.dagstuhl.de/opus/volltexte/2020/12762

20.

Iwamoto, C., Ide, T.: Five cells and tilepaint are NP-complete. IEICE Trans. Inf. Syst. 105(3), 508–516 (2022). https://www.jstage.jst.go.jp/article/transinf/E105.D/3/E105.D_2021FCP0001/_pdf

21.

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

22.

Saha, S., Demaine, E.D.: ZHED is NP-complete. In: Proceedings of the 34th Canadian Conference on Computational Geometry (CCCG 2022) (2022). https://erikdemaine.org/papers/Zhed_CCCG2022/paper.pdf

23.

Nikoli: Juosan-nikoli. https://www.nikoli.co.jp/en/puzzles/juosan/ (2022). Accessed 30 Nov 2022

24.

Ammar, M.T., Arzaki, M., Wulandari, G.S.: Note on algorithmic investigations of Juosan puzzles. (to appear) Jurnal Ilmu Komputer dan Informasi (J. Comput. Sci. Inf.) (2023). https://github.com/tsaqifammar/juosan-backtracking/blob/main/preprint/Preprint-AlgoJuosan.pdf

25.

Putra, M.I., Arzaki, M., Wulandari, G.S.: Solving Yin-Yang puzzles using exhaustive search and Prune-and-search algorithms. (IJCSAM) Int. J. Comput. Sci. Appl. Math. 8(2), 52–65 (2022)

26.

Reinhard, E.C., Arzaki, M., Wulandari, G.S.: Solving Tatamibari puzzle using exhaustive search approach. Indones. J. Comput. (Indo-JC) 7(3), 53–80 (2022). https://socj.telkomuniversity.ac.id/ojs/index.php/indojc/article/view/675

27.

Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems, 2nd edn. Cambridge university press (2004)

28.

Ben-Ari, M.: Mathematical Logic for Computer Science, 3rd edn. Springer Science & Business Media (2012)

29.

W., D.: Encoding SAT EqualsK constraint with two possible values. Computer Science Stack Exchange. https://cs.stackexchange.com/q/159821 (version: 2023-05-09)

30.

Sinz, C.: Towards an optimal CNF encoding of boolean cardinality constraints. In: Principles and Practice of Constraint Programming-CP 2005: 11th International Conference, CP 2005, Sitges, Spain, 1–5 October 2005. Proceedings of vol. 11, pp. 827–831. Springer (2005)

31.

Frisch, A.M., Giannaros, P.A.: SAT encodings of the at-most-k constraint: Some old, some new, some fast, some slow (2010)

32.

Bittner, P.M., Thüm, T., Schaefer, I.: SAT Encodings of the at-most-k constraint: a case study on configuring university courses. In: Software Engineering and Formal Methods: 17th International Conference, SEFM 2019, Oslo, Norway, 18–20 September 2019, Proceedings of vol. 17, pp. 127–144. Springer (2019)

33.

Nguyen, V.H., Nguyen, V.Q., Kim, K., Barahona, P.: Empirical study on SAT-encodings of the at-most-one constraint. In: The 9th International Conference on Smart Media and Applications, pp. 470–475 (2020)

34.

Hořeňovský, M.: 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/ (2019). Accessed 22 May 2023

35.

Prechelt, L.: An empirical comparison of seven programming languages. Computer 33(10), 23–29 (2000)CrossRef

36.

Otto Janko: Juosan. https://www.janko.at/Raetsel/Juosan/index.htm (2022). Accessed 11 Oct 2022

Title: Efficient SAT-Based Approach for Solving Juosan Puzzles
Authors: Muhammad Tsaqif Ammar
Muhammad Arzaki
Gia Septiana Wulandari
Publisher: Springer Nature Singapore
Book: Applied and Computational Mathematics
Print ISBN: 978-981-9721-35-1

Electronic ISBN: 978-981-9721-36-8

Copyright Year: 2024
DOI: https://doi.org/10.1007/978-981-97-2136-8_16

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"