Top

Published in:

2024 | OriginalPaper | Chapter

Modeling Path Puzzles as SAT Problems and How to Solve Them

Authors : Joshua Erlangga Sakti, 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

This paper discusses a SAT-based approach for solving the Path Puzzles—one-player paper-and-pencil puzzles recently proven NP-complete in 2020. The properties and rules of Path Puzzles are encoded into propositional formulas in Conjunctive Normal Forms (CNF). We describe the step-by-step derivation for such formulas and analyze the number of clauses and variables used to express them. Experimental results show that our declarative SAT-based solver in PySAT outperforms the conventional imperative backtracking technique for solving 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 Efficient SAT-Based Approach for Solving Juosan Puzzles

next chapter A Trustworthiness Scoring Model for Reviews Using a Graph Structure

Notice that we can define \(C_{i,j}\) as a disjunction of \(P_{i,j,s}\) where \(1 \le s \le \ell \).

It is possible to make a tighter lower bound for \(lbRow\) and \(lbCol\) as follows: (1) if a door cell is located at a column (resp. row) without numerical constraint, the lower bound for the corresponding column (resp. row) is \(1\) (or 2 if both door cells are located in the same column (resp. row)); (2) every row (resp. column) without numerical constraint located between two rows (resp. columns) with positive numerical constraints has a lower bound of \(1\). However, we refrain from using this lower bound to avoid cumbersome and complicated analysis.

We construct the instances and their corresponding solutions using Z3 Theorem Prover.

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

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

Bosboom, J., Demaine, E.D., Demaine, M.L., Hesterberg, A., Kimball, R., Kopinsky, J.: Path puzzles: discrete tomography with a path constraint is hard. Graphs Comb. 36(2), 251–267 (2020). https://link.springer.com/content/pdf/10.1007/s00373-019-02092-5.pdf

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

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

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

Ueda, N., Nagao, T.: NP-completeness results for Nonogram via parsimonious reductions. Technical report, Department of Computer Science, Tokyo Institute of Technology (1996)

Hoogeboom, H.J., Kosters, W.A., van Rijn, J.N., Vis, J.K.: Acyclic constraint logic and games. ICGA J. 37(1), 3–16 (2014)CrossRef

Ryser, H.: Combinatorial properties of matrices of zeros and ones. Can. J. Math. 9, 371–377 (1957)MathSciNetCrossRef

10.

Herman, G.T., Kuba, A.: Discrete Tomography: Foundations, Algorithms, and Applications. Springer Science & Business Media (2012)

11.

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)

12.

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)

13.

Sakti, J.E., Arzaki, M., Wulandari, G.S.: A backtracking approach for solving path puzzles. Preprint (2023). https://github.com/joshuagatizz/path-puzzles-backtracking-solver/blob/main/preprint/Preprint-BacktrackingPathPuzzle.pdf

14.

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

15.

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

16.

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

17.

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

18.

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)

19.

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 14, pp. 560–565. Springer (2008)

20.

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

21.

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)

22.

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)

23.

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

24.

Demaine, E.D.: Path puzzles font. https://github.com/edemaine/font-pathpuzzles. Accessed 11 Oct 2022

25.

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

26.

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

27.

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

28.

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 17, pp. 127–144. Springer (2019)

29.

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)

30.

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

Title: Modeling Path Puzzles as SAT Problems and How to Solve Them
Authors: Joshua Erlangga Sakti
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_17

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"