Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(3)
Polynomial Time
satisabilit y
Conjunctive Normal Form
Related Publications
(3)
Sudoku as a Constraint Problem
A SATbased Sudoku Solver?
MITS: A MixedInitiative Intelligent Tutoring System for Sudoku
Subscribe
Academic
Publications
Sudoku as a SAT Problem
Sudoku as a SAT Problem
Edit
Sudoku as a SAT Problem
(
Citations: 25
)
BibTex

RIS

RefWorks
Download
Unknown
Abstract Sudoku is a very simple and wellknown 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 polynomialtime 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.
Conference:
Artificial Intelligence and Mathematics  AI&M
Cumulative
Annual
Citation Context
(16)
...[
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 Bauer
,
et al.
Don't care in SMT: building flexible yet efficient abstraction/refinem...
...normal form. Following [
3
], a sudoku square of order n can...
Daniel DiazPernil
,
et 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 KOREKAWA
,
et 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 stateoftheart SAT solver (MiniSat 2 beta [14] on TABLE III: Comparison of FTP’09, ECP and SAT software solver computation times in seconds...
Michael Dittrich
,
et al.
Solving Sudokus through an incidence matrix on an FPGA
...Lynce and Ouaknine apply various SATbased 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 Henz
,
et al.
SudokuSatA Tool for Analyzing Difficult Sudoku Puzzles
References
(8)
Exploring the Computational Tradeoff of more Reasoning and Less Searching
(
Citations: 19
)
Fahiem Bacchus
Conference:
Theory and Applications of Satisfiability Testing
, 2002
Effective Preprocessing with HyperResolution and Equality Reduction
(
Citations: 74
)
Fahiem Bacchus
,
Jonathan Winter
Conference:
Theory and Applications of Satisfiability Testing
, pp. 341355, 2003
The complexity of completing partial Latin squares
(
Citations: 70
)
C. J. Colbourn
Journal:
Discrete Applied Mathematics  DAM
, vol. 8, no. 1, pp. 2530, 1984
Experimental Results on the Crossover Point in Satisfiability Problems
(
Citations: 198
)
James M. Crawford
,
Larry D. Auton
Conference:
National Conference on Artificial Intelligence  AAAI
, pp. 2127, 1993
A Computing Procedure for Quantification Theory
(
Citations: 1436
)
Martin Davis
,
Hilary Putnam
Journal:
Journal of The ACM  JACM
, vol. 7, no. 3, pp. 201215, 1960
Sort by:
Citations
(25)
Don't care in SMT: building flexible yet efficient abstraction/refinement solvers
(
Citations: 1
)
Andreas Bauer
,
Martin Leucker
,
Christian Schallhart
,
Michael Tautschnig
Journal:
International Journal on Software Tools for Technology Transfer  STTT
, vol. 12, no. 1, pp. 2337, 2010
Solving Sudoku with genetic operations that preserve building blocks
(
Citations: 1
)
Yuji Sato
,
Hazuki Inoue
Published in 2010.
Solving sudoku with Membrane Computing
Daniel DiazPernil
,
Carlos M. FernandezMarquez
,
M. GarcíaQuismondo
,
M. A. GutiérrezNaranjo
,
M. A. MartínezdelAmor
Published in 2010.
Rating and Generating Sudoku Puzzles
Shanchen Pang
,
Eryan Li
,
Tao Song
,
Peng Zhang
Conference:
International Workshop on Education Technology and Computer Science  ETCS
, 2010
"Solution Path": The Structure of the Solution Steps for Pencil Puzzle
Takashi KOREKAWA
,
Kanako KOMIYA
,
Yoshiyuki KOTANI
Conference:
International Conference on Technologies and Applications of Artificial Intelligence  TAAI
, 2010