Isomorphism between Sudoku and Proof Systems and Its Application in Sudoku Solving

Proceedings

article

Jakub Dakowski¹ 

[1] Department of Logic and Cognitive Science, Adam Mickiewicz University

关键词: logic;    proof theory;    sudoku;    puzzle;    consequence operation;   

DOI  :  10.3390/proceedings2022081078

学科分类：社会科学、人文和艺术（综合）

来源: mdpi

【 摘 要 】

(1) Introduction: While automatic Sudoku solvers are a well-known area of study in formal sciences, there has been little to no progress when it comes to describing the proving process as analogous to Sudoku solving. (2) Materials and Methods: This paper proposes two methods of solving Sudokus automatically: one using Hilbert systems, the other with an additional contradiction rule. (3) Results: While the first algorithm was not complete, it seems that the second one is. It was able to solve most of the provided test cases in under a second. (4) Discussion: Different work already suggests this concept for a Sudoku solver. However, it comes from a different theoretic standpoint. Future work in this field might include incorporating the results of proof theory or searching for a Sudoku solvable for every possible substitution.

【 授权许可】

CC BY