Academic
Publications
Sudoku as a SAT Problem

Sudoku as a SAT Problem

Sudoku as a SAT Problem   (Citations: 25)
BibTex | RIS | RefWorks Download
Unknown
Abstract Sudoku is a very simple and well-known puzzle that has achieved international popularity in the recent past. This paper addresses the problem of encoding Sudoku puzzles into conjunctive normal form (CNF), and subsequently solving them using polynomial-time propositional satisabilit y (SAT) inference techniques. We introduce two straightforward SAT encodings for Sudoku: the minimal encoding and the extended encoding. The minimal encoding suces,to characterize Sudoku puzzles, whereas the extended encoding adds redundant clauses to the minimal encoding. Experimental results demonstrate that, for thousands of very hard puzzles, inference techniques struggle to solve these puzzles when using the minimal encoding. However, using the extended encoding, unit propagation is able to solve about half of our set of puzzles. Nonetheless, for some puzzles more sophisticated inference techniques are required.
Cumulative Annual
    • ...[18,31]). Having a solver at hand which solves Boolean as well as linear problems, however, the Sudoku puzzle can be tackled more efficiently as a mixed problem and the encoding is more natural as it can make use of integers...

    Andreas Baueret al. Don't care in SMT: building flexible yet efficient abstraction/refinem...

    • ...normal form. Following [3], a sudoku square of order n can...

    Daniel Diaz-Pernilet al. Solving sudoku with Membrane Computing

    • ...The methods for formulation of number place have shown in [5] and [6] the former treats the problem as CSP (Constraint Satisfaction problem), and latter treats it as SAT (SATisfiability) problem...

    Takashi KOREKAWAet al. "Solution Path": The Structure of the Solution Steps for Pencil Puzzle

    • ...Others modelled Sudoku as a Satisfiability Problem (SAT) [6], [7] and as a Constraint Satisfaction Problem (CSP) [8]...
    • ...To do so, the puzzles were transformed into a SAT problem as described in [6] (extended coding) and were solved with a state-of-the-art SAT solver (MiniSat 2 beta [14] on TABLE III: Comparison of FTP’09, ECP and SAT software solver computation times in seconds...

    Michael Dittrichet al. Solving Sudokus through an incidence matrix on an FPGA

    • ...Lynce and Ouaknine apply various SAT-based resolution techniques to Sudoku [10]...
    • ...We use the following extended encoding of Sudoku, given by Lynce and Ouaknine [10]...
    • ...The variable sxyz is assigned to TRUE if and only if the cell in row x and column y contains the digit z. The following conjunctions of clauses combined make up the extended encoding (for a detailed explanation, see [10]):...
    • ...The experiments reported by Lynce and Ouaknine [10] use a set of 24,260 very difficult Sudoku puzzles collected by Gordon Royle [13]...
    • ...A common assumption at the time of publication of previous studies on using AI techniques for Sudoku [10, 16, 14, 6] was that the most difficult Sudoku puzzles would be minimal...
    • ...Lynce and Ouaknine [10] report that FLP solves all puzzles listed by Royle [13], a fact that we verified with SUDOKUSAT...

    Martin Henzet al. SudokuSat-A Tool for Analyzing Difficult Sudoku Puzzles

Sort by: