Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Kongresse
Themenseiten
Künstliche Intelligenz Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Veranstaltungskalender Awards MyNewsletter Firmensuche
Kunden Login
Über Einzelzugang informieren
Über Unternehmenszugang informieren
Referenzkunden
Zukunftswerkstatt Sales Excellence 2025 | 08. Mai 2025

KI als Booster im Vertrieb

Lernen Sie von Digital-Experten, wie der gezielte Einsatz von KI-Unterstützung Ihrem Unternehmen in vielen Bereichen hilft, im Vertrieb einen Schritt voraus zu sein. Jetzt wieder live vor Ort teilnehmen in Frankfurt am Main!
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Kapitel lesen Erstes Kapitel lesen

2024 | OriginalPaper | Buchkapitel

Efficient SAT-Based Approach for Solving Juosan Puzzles

verfasst von : Muhammad Tsaqif Ammar, Muhammad Arzaki, Gia Septiana Wulandari

Erschienen in: Applied and Computational Mathematics

Verlag: Springer Nature Singapore

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Vorheriges Kapitel Dynamic Response of Floating Crane During Lifting Operation: A Parametric Study
Nächstes Kapitel Modeling Path Puzzles as SAT Problems and How to Solve Them
Fußnoten
1
Two Boolean formulas \(\phi \) and \(\psi \) are equisatisfiable if and only if the satisfiability of \(\phi \) implies the satisfiability of \(\psi \), and conversely.
 
Literatur
1.
Hearn, R.A., Demaine, E.D.: Games, Puzzles, and Computation. CRC Press (2009)
2.
Lynce, I., Ouaknine, J.: Sudoku as a SAT Problem. In: AI &M (2006)
3.
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)
4.
Henz, M., Truong, H.M.: Sudokusat-a tool for analyzing difficult sudoku puzzles. In: Tools and Applications with Artificial Intelligence, pp. 25–35 (2009)
5.
Pfeiffer, U., Karnagel, T., Scheffler, G.: A Sudoku-solver for large puzzles using SAT. In: LPAR Short Papers (Yogyakarta), pp. 52–57 (2010)
6.
Bright, C., Gerhard, J., Kotsireas, I., Ganesh, V.: Effective problem solving using SAT solvers. In: Maple Conference, pp. 205–219. Springer (2019)
7.
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)
8.
9.
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.
16.
17.
18.
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.
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.
23.
24.
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.
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.
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.
35.
Prechelt, L.: An empirical comparison of seven programming languages. Computer 33(10), 23–29 (2000)CrossRef
36.
Metadaten
Titel
Efficient SAT-Based Approach for Solving Juosan Puzzles
verfasst von
Muhammad Tsaqif Ammar
Muhammad Arzaki
Gia Septiana Wulandari
Copyright-Jahr
2024
Verlag
Springer Nature Singapore
Buch
Applied and Computational Mathematics

Print ISBN: 978-981-9721-35-1

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

Copyright-Jahr: 2024

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

Premium Partner

    Marktübersichten

    Die im Laufe eines Jahres in der „adhäsion“ veröffentlichten Marktübersichten helfen Anwendern verschiedenster Branchen, sich einen gezielten Überblick über Lieferantenangebote zu verschaffen. 

    Zur Marktübersicht
    Bildnachweise