论文标题
在sudoku中的可得性
Deducibility in Sudoku
论文作者
论文摘要
在本文中，我们提供了一种形式主义，即sudoku逻辑，其中解决方案在逻辑上是可以推论的，如果对于网格的每个单元格，我们可以证明除了单个选项之外都可以排除所有内容。我们证明，Sudoku逻辑的演绎系统是合理而完整的，因此，当且仅当它具有可疑的解决方案时，我们证明了Sudoku拼图具有独特的解决方案。然后，使用Adler和Adler对基本的Sudoku转换分类，然后我们将Sudoku中对称性的概念形式化，并提供了Gurth对称放置定理的正式证明。在总结部分中，我们提出了一个Sudoku公式，该公式捕获了具有独特解决方案的Sudoku网格的想法。事实证明，这个公式是sudoku逻辑的公理，使我们有可能向sudoku社区提供解决唯一性争议的解决：如果我们接受本文所介绍的sudoku逻辑，就没有争议！唯一性是公理，并且与任何其他公理一样，可以在任何sudoku扣除中自由使用。
In this paper we provide a formalism, Sudoku logic, in which a solution is logically deducible if for every cell of the grid we can provably exclude all but a single option. We prove that the deductive system of Sudoku logic is sound and complete, and as a consequence of that we prove that a Sudoku puzzle has a unique solution if and only if it has a deducible solution. Using the classification of fundamental Sudoku transformations by Adler and Adler we then formalize the notion of symmetry in Sudoku and provide a formal proof of Gurth's Symmetrical Placement Theorem. In the concluding section we present a Sudoku formula that captures the idea of a Sudoku grid having a unique solution. It turns out that this formula is an axiom of Sudoku logic, making it possible for us to offer to the Sudoku community a resolution of the Uniqueness Controversy: if we accept Sudoku logic as presented in this paper, there is no controversy! Uniqueness is an axiom and, as any other axiom, may freely be used in any Sudoku deduction.
