Please wait ...

Benchmark(s) have been added to cart.

Tag has been added.

• Login
• Register
• Links
• FAQs
• Contact

Navigation

• Instance
  • Show Instances
• Problem
  • Show Problems
• Show Tags
• Search
• Cart

Encoding gen_sudoku.gringo

Name	gen_sudoku.gringo
Class Tree	[Root]    Puzzles (51)    Grid (17)    Su-Doku (3)
Submitter	Martin Gebser
Author	Martin Gebser
Description	This encoding generates Sudoku puzzles having a unique solution, while removing any clue (neglecting a preassigned cell) leads to alternative solutions. To randomize the generation of Sudoku puzzles, one can use the "shuffle" tool available at: http://www.tcs.hut.fi/Software/asptools/ The meanings of the output atoms are as follows: - cell(X,Y): there is a grid cell (X,Y) - clue(X,Y,V): grid cell (X,Y) is preassigned to value V - assign(X,Y,V): grid cell (X,Y) is assigned to value V in the unique solution Note that clue(X,Y,V) implies assign(X,Y,V) for all X,Y,V.
Created	2010-03-19 19:52
Modified	2010-03-20 17:25
Languages	Gringo 2.0.2
Language Features	Cardinality constraints Disjunction Choice rules
Compatible Instance Classes
Input Predicates
Output Predicates	assign/3 cell/2 clue/3
Encoding Parameter	size
Standalone	Yes
Tags
Attributes
Content	#const size=3. % Describe Sudoku grid dim(1..size*size). cell(X,Y) :- dim(X;Y). sub(X,Y,((((X-1) / size) * size) + ((Y-1) / size)) + 1) :- cell(X,Y). % Guess clues (in order) { clue(1,Y,N) : dim(N) : N <= Y } 1 :- dim(Y). { clue(X,Y,N) : dim(N) } 1 :- cell(X,Y), 1 < X. clue(X,Y) :- clue(X,Y,N). clue(N) :- clue(X,Y,N). :- dim(S), not dim(S+1), not clue(S-1), 1 < S. clued(X,Y,N) :- clue(X,Y,N). clued(X,Y+1,N) :- clued(X,Y,N), cell(X,Y), dim(N), dim(Y+1). clued(X+1,1,N) :- clued(X,Y,N), cell(X,Y), dim(N), not dim(Y+1), dim(X+1). :- clue(X,Y,N), not clued(X,Y,N-1), 1 < N. % Construct witness w.r.t. clues 1 { assign(X,Y,N) : dim(N) } 1 :- cell(X,Y). :- clue(X,Y,N), not assign(X,Y,N). 1 { assign(X,Y,N) : dim(Y) } 1 :- dim(X), dim(N). 1 { assign(X,Y,N) : dim(X) } 1 :- dim(Y), dim(N). 1 { assign(X,Y,N) : sub(X,Y,S) } 1 :- dim(S), dim(N). % Verify uniqueness of witness altassign(X,Y,N) : dim(N) :- cell(X,Y). bot :- altassign(X,Y,N), clue(X,Y), not clue(X,Y,N). keep(X,Y) :- assign(X,Y,N), altassign(X,Y,N). bot :- keep(X,Y) : cell(X,Y). bot :- 2 { altassign(X,Y,N) : dim(Y) }, dim(X), dim(N). bot :- 2 { altassign(X,Y,N) : dim(X) }, dim(Y), dim(N). bot :- 2 { altassign(X,Y,N) : sub(X,Y,S) }, dim(S), dim(N). altassign(X,Y,N) :- bot, cell(X,Y), dim(N). :- not bot. % Construct alternative witnesses altering one clue 1 { reassign(XX,YY,X,Y,N) : dim(N) } 1 :- clue(XX,YY), cell(X,Y). :- clue(X,Y,N), reassign(X,Y,X,Y,N). :- clue(X,Y,N), clue(XX, Y), X != XX, not reassign(XX, Y,X,Y,N). :- clue(X,Y,N), clue(XX,YY), Y != YY, not reassign(XX,YY,X,Y,N). 1 { reassign(XX,YY,X,Y,N) : dim(Y) } 1 :- clue(XX,YY), dim(X), dim(N). 1 { reassign(XX,YY,X,Y,N) : dim(X) } 1 :- clue(XX,YY), dim(Y), dim(N). 1 { reassign(XX,YY,X,Y,N) : sub(X,Y,S) } 1 :- clue(XX,YY), dim(S), dim(N). #hide. #show cell/2. #show clue/3. #show assign/3.