Abstract
Sudoku puzzles enjoy world-wide popularity, and a large community of puzzlers is hoping for ever more difficult puzzles. A crucial step for generating difficult Sudoku puzzles is the fast assessment of the difficulty of a puzzle. In a study in 2006, it has been shown that SAT solving provides a way to efficiently differentiate between Sudoku puzzles according to their difficulty, by analyzing which resolution technique solves a given puzzle. This paper shows that one of these techniques—unit resolution with failed literal propagation—does not solve a recently published Sudoku puzzle called AI Escargot, claimed to be the world’s most difficult. The technique is also unable to solve any of a list of difficult puzzles published after AI Escargot, whereas it solves all previously studied Sudoku puzzles. We show that the technique can serve as an efficient and reliable computational method for distinguishing the most difficult Sudoku puzzles. As a proof-of-concept for an efficient difficulty checker, we present the tool SudokuSat that categorizes Sudoku puzzles with respect to the resolution technique required for solving them.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
AFP. Mathematician claims to have penned hardest Sudoku. USA Today (November 2006)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the Association for Computing Machinery 5(7), 394–397 (1962)
Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the Association for Computing Machinery 7, 201–215 (1960)
Felgenhauer, B., Jarvis, F.: Enumerating possible Sudoku grids (2005), http://www.afjarvis.staff.shef.ac.uk/sudoku/sudoku.pdf
Hanson, B.: Sudoku Assistant/Solver. Online software written in JavaScript (2007), http://www.stolaf.edu/people/hansonr/sudoku/
Holst, C.K.: Sudoku—an excercise in constraint programming in Visual Prolog 7. In: 1st Visual Prolog Applications and Language Conference, VIP-ALC 2006, Faro, Portugal (April 2006)
Inkala, A.: AI Escargot—The Most Difficult Sudoku Puzzle, Lulu, Finland (2007) ISBN 978-1-84753-451-4
Juillerat, N.: Sudoku Explainer. Version 1.2 (December 2006), http://diuf.unifr.ch/people/juillera/Sudoku/Sudoku.html
Knuth, D.E.: Dancing links. In: Davies, J., Roscoe, B., Woodcock, J. (eds.) Millenial Perspectives in Computer Science, pp. 187–214. Palgrave, Houndmills (2000)
Lynce, I., Ouaknine, J.: Sudoku as a SAT problem. In: Berstein, S.Z. (ed.) Proceedings of the 9th International Symposium on Artificial Intelligence and Mathematics, AIMATH 2006, Fort Lauderdale, Florida, USA ( January 2006)
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference, Las Vegas, USA (June 2001)
ravel. The hardest sudokus. Sudoku Players’ Forums (January 25, 2007), http://www.sudoku.com/forums/viewtopic.php?t=4212&start=587
Royle, G.: Minimum sudoku (2007), http://people.csse.uwa.edu.au/gordon/sudokumin.php
Simonis, H.: Sudoku as a constraint problem. In: Proceedings of the CP Workshop on Modeling and Reformulating Constraint Satisfaction Problems, Sitges, Spain, pp. 13–27 (October 2005)
Torres, P., Lopez, P.: Overview and possible extensions of shaving techniques for job-shop problems. In: 2nd International Workshop on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, CP-AI-OR 2000, IC-PARC, UK, pp. 181–186 (March 2000)
Weber, T.: A SAT-based Sudoku solver. In: Geoff Sutclife and Andrei Voronkov, editors, 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR 2005, pp. 11–15, Montego Bay, Jamaica (December 2005) (short paper Proceedings)
Yato, T.: Complexity and completeness of finding another solution and its application to puzzles. Master’s thesis, Univ. of Tokyo, Dept. of Information Science, Faculty of Science, Hongo 7-3-1, Bunkyo-ku, Tokyo 113, JAPAN (January 2003), http://www-imai.is.s.u-tokyo.ac.jp/~yato/data2/MasterThesis.ps
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Henz, M., Truong, HM. (2009). SudokuSat—A Tool for Analyzing Difficult Sudoku Puzzles. In: Koutsojannis, C., Sirmakessis, S. (eds) Tools and Applications with Artificial Intelligence. Studies in Computational Intelligence, vol 166. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-88069-1_3
Download citation
DOI: https://doi.org/10.1007/978-3-540-88069-1_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-88068-4
Online ISBN: 978-3-540-88069-1
eBook Packages: EngineeringEngineering (R0)