(mod SUDOKU is protecting NAT . protecting QID . protecting CONVERSION . --- Description. Sudoku Solver with Strategies --- Author: Gustavo Santos-Garcia & Miguel Palomino --- email: santos@usal.es, miguelpt@sip.ucm.es --- Date. Feb 10, 2005 --- Version: 1.2.2 *** mod CONFIGURATION-FORMAT is sorts Attribute AttributeSet . subsort Attribute < AttributeSet . op none : -> AttributeSet . op _`,_ : AttributeSet AttributeSet -> AttributeSet [ctor assoc comm id: none format (m! o sm! o)] . sorts Oid Cid Object Msg Configuration . subsort Object Msg < Configuration . op <_:_|_> : Oid Cid AttributeSet -> Object [ctor object format (n r! o g o tm! ot d)] . op none : -> Configuration . op __ : Configuration Configuration -> Configuration [ctor config assoc comm id: none] . *** endm CONFIGURATION-FORMAT *** Cell (Grid, Given, Value and Number) definitions ops cell rows : -> Cid . op id : Nat Nat -> Oid . op msg : Qid -> Msg [ctor format (nb! r!)] . ops (grd`:_) (giv`:_) (num`:_) : Nat -> Attribute . op pss`:_ : Set -> Attribute . op val`:_ : List -> Attribute . ********* Initialization of the sudoku ********* --- Initial position of a sudoku according to the grid "grid". sort Sudoku . op <<_>> : Configuration -> Sudoku . op none : -> Sudoku . op __ : Sudoku Sudoku -> Sudoku [ctor config assoc comm id: none] . op sudoku : -> Sudoku . eq sudoku = << msg('SearchingSolution) fill(1, 1, ( 0 ; 9 ; 0 ; 7 ; 0 ; 0 ; 8 ; 6 ; 0 ; 0 ; 3 ; 1 ; 0 ; 0 ; 5 ; 0 ; 2 ; 0 ; 8 ; 0 ; 6 ; 0 ; 0 ; 0 ; 0 ; 0 ; 0 ; 0 ; 0 ; 7 ; 0 ; 5 ; 0 ; 0 ; 0 ; 6 ; 0 ; 0 ; 0 ; 3 ; 0 ; 7 ; 0 ; 0 ; 0 ; 5 ; 0 ; 0 ; 0 ; 1 ; 0 ; 7 ; 0 ; 0 ; 0 ; 0 ; 0 ; 0 ; 0 ; 0 ; 1 ; 0 ; 9 ; 0 ; 2 ; 0 ; 6 ; 0 ; 0 ; 3 ; 5 ; 0 ; 0 ; 5 ; 4 ; 0 ; 0 ; 8 ; 0 ; 7 ; 0 ) ) >> . op fill : Nat Nat List -> Object . eq fill( R, C, (N ; LL)) = if C == 9 then < id(R, C) : cell | grd : grd(R, C), pss : pss(N), num : num(N) > fill(s R, 1, LL) else < id(R, C) : cell | grd : grd(R, C), pss : pss(N), num : num(N) > fill( R, s C, LL) fi . eq fill(R, C, N) = < id(R, C) : cell | grd : grd(R, C), pss : pss(N), num : num(N) > . op grd : Nat Nat -> Nat . eq grd(R, C) = (sd(R, 1) quo 3) * 3 + (sd(C, 1) quo 3) + 1 . op pss : Nat -> Set . eq pss(N) = if N == 0 then (1 2 3 4 5 6 7 8 9) else (N) fi . op num : Nat -> Nat . eq num(N) = if N == 0 then 9 else 1 fi . ********* Variables ********* var VOid : Oid . var VCid : Cid . var VMsg : Msg . vars VConf VConf' : Configuration . vars At At1 At2 At3 At4 At5 At6 At7 At8 At9 : AttributeSet . vars N N' N1 N2 N3 N4 N5 N6 N7 N8 N9 R R' R1 R2 R3 R4 R5 R6 R7 R8 R9 : Nat . vars C C' C1 C2 C3 C4 C5 C6 C7 C8 C9 G G' G1 G2 G3 G4 G5 G6 G7 G8 G9 P P' P1 P2 P3 : Nat . vars LP LP' LP1 LP2 LP3 LP4 LP5 LP6 LP7 LP8 LP9 : Set . var LL : List . ********* List and Set ********* sorts List Set . subsort Nat < List . subsort Nat < Set . op _;_ : Nat List -> List . op empty : -> Set [ctor] . op __ : Set Set -> Set [ctor assoc comm id: empty] . ops inters union : Set Set -> Set [comm assoc memo] . op card : Set -> Nat . op minus : Set Set -> Set . op _in_ : Nat Set -> Bool . ops (_subset_) (disj) : Set Set -> Bool . eq inters((P LP), (P LP')) = P inters(LP, LP') . eq inters(LP, LP') = empty [owise] . eq union((P LP), (P LP')) = P union(LP, LP') . eq union(LP, LP') = (LP LP') [owise] . eq card(N LP) = s card(LP) . eq card(empty) = 0 . eq minus((P LP), (P LP')) = minus(LP, LP') . eq minus(LP, LP') = LP [owise] . eq N in (N LP) = true . eq N in LP = false [owise] . eq LP subset LP' = (inters(LP, LP') == LP ) . eq disj(LP, LP') = (inters(LP, LP') == empty) . op same : Nat Nat Nat -> Bool . op same : Nat Nat Nat Nat -> Bool . op same : Nat Nat Nat Nat Nat Nat Nat Nat Nat -> Bool . eq same(N1, N2, N3) = (N1 == N2) and (N1 == N3) . eq same(N1, N2, N3, N4) = (N1 == N2) and (N1 == N3) and (N1 == N4) . eq same(R1, R2, R3, R4, R5, R6, R7, R8, R9) = ((R1 == R2) and (R1 == R3) and (R1 == R4) and (R1 == R5) and (R1 == R6) and (R1 == R7) and (R1 == R8) and (R1 == R9)) . ********* Configuration functions ********* ops maxCard minCard betCard : Configuration -> Nat [memo] . eq maxCard(none) = 0 . eq minCard(none) = 9 . eq betCard(none) = 9 . eq maxCard(VConf < VOid : VCid | num : N, At >) = max(N, maxCard(VConf)) . eq minCard(VConf < VOid : VCid | num : N, At >) = min(N, minCard(VConf)) . eq betCard(VConf < VOid : VCid | num : N, At >) = if N == 1 then betCard(VConf) else min(N, betCard(VConf)) fi . ********* Equations and rewrite rules ********* --- [simplify1st] If only one number is possible in a cell, then we remove --- this number from the set of possible numbers in all the other cells in the --- same row, column or grid. crl [simplify1st] : < id(R1, C1) : cell | grd : G1, pss : P, num : 1 > < id(R2, C2) : cell | grd : G2, pss : (P LP), num : N > => < id(R1, C1) : cell | grd : G1, pss : P, num : 1 > < id(R2, C2) : cell | grd : G2, pss : LP, num : sd(N,1) > if ((R1 == R2) or (C1 == C2) or (G1 == G2)) . --- [simplify2nd] If two cells in the same row (column or grid) have the same --- set of possible numbers and its cardinality is 2, then those numbers can --- be removed from the sets of possible numbers of every other cell in the --- same row (column or grid). crl [simplify2nd] : < id(R1, C1) : cell | grd : G1, pss : (P P'), num : 2 > < id(R2, C2) : cell | grd : G2, pss : (P P'), num : 2 > < id(R3, C3) : cell | grd : G3, pss : (P LP3), num : N3 > => < id(R1, C1) : cell | grd : G1, pss : (P P'), num : 2 > < id(R2, C2) : cell | grd : G2, pss : (P P'), num : 2 > < id(R3, C3) : cell | grd : G3, pss : LP3, num : sd(N3,1) > if (same(R1, R2, R3) or same(C1, C2, C3) or same(G1, G2, G3)) . --- [simplify3rd] If three cells in the same row (column or grid) have the --- same set of possible numbers and its cardinality is 3, then those numbers --- can be removed from the sets of possible numbers of every other cell in --- the same row (column or grid). crl [simplify3rd] : < id(R1, C1) : cell | grd : G1, pss : (P1 P2 P3), num : 3 > < id(R2, C2) : cell | grd : G2, pss : (P2 LP2), num : N2 > < id(R3, C3) : cell | grd : G3, pss : (P3 LP3), num : N3 > < id(R4, C4) : cell | grd : G4, pss : LP4, num : N4 > => < id(R1, C1) : cell | grd : G1, pss : (P1 P2 P3), num : 3 > < id(R2, C2) : cell | grd : G2, pss : (P2 LP2), num : N2 > < id(R3, C3) : cell | grd : G3, pss : (P3 LP3), num : N3 > < id(R4, C4) : cell | grd : G4, pss : minus(LP4, (P1 P2 P3)), num : card(minus(LP4, (P1 P2 P3))) > if (same(R1, R2, R3, R4) or same(C1, C2, C3, C4) or same(G1, G2, G3, G4)) and (LP2 subset (P1 P3)) and (LP3 subset (P1 P2)) and not disj((P1 P2 P3), LP4) . --- [onlyOneNumber] When a number is not possible in any cell of a row (column --- or grid) but one, and the cardinality of the set of possible numbers for --- this cell is greater than one, then this set can become a singleton --- containing that number. crl [onlyOneNumber] : < id(R1, C1) : cell | grd : G1, pss : (P LP1), At1 > < id(R2, C2) : cell | grd : G2, pss : LP2, At2 > < id(R3, C3) : cell | grd : G3, pss : LP3, At3 > < id(R4, C4) : cell | grd : G4, pss : LP4, At4 > < id(R5, C5) : cell | grd : G5, pss : LP5, At5 > < id(R6, C6) : cell | grd : G6, pss : LP6, At6 > < id(R7, C7) : cell | grd : G7, pss : LP7, At7 > < id(R8, C8) : cell | grd : G8, pss : LP8, At8 > < id(R9, C9) : cell | grd : G9, pss : LP9, At9 > => < id(R1, C1) : cell | grd : G1, pss : P, num : 1 > < id(R2, C2) : cell | grd : G2, pss : LP2, At2 > < id(R3, C3) : cell | grd : G3, pss : LP3, At3 > < id(R4, C4) : cell | grd : G4, pss : LP4, At4 > < id(R5, C5) : cell | grd : G5, pss : LP5, At5 > < id(R6, C6) : cell | grd : G6, pss : LP6, At6 > < id(R7, C7) : cell | grd : G7, pss : LP7, At7 > < id(R8, C8) : cell | grd : G8, pss : LP8, At8 > < id(R9, C9) : cell | grd : G9, pss : LP9, At9 > if (same(R1, R2, R3, R4, R5, R6, R7, R8, R9) or same(C1, C2, C3, C4, C5, C6, C7, C8, C9) or same(G1, G2, G3, G4, G5, G6, G7, G8, G9)) and not (P in union(LP2, LP3, LP4, LP5, LP6, LP7, LP8, LP9)) . --- [onlyTwoNumbers] When two numbers p1 and p2 are not possible in any --- cell of a row (column or grid) but two, and the sets of possible numbers --- for these cells have cardinality greater than two, then these sets can --- become p1, p2. crl [onlyTwoNumbers] : < id(R1, C1) : cell | grd : G1, pss : (P1 P2 LP1), num : N1 > < id(R2, C2) : cell | grd : G2, pss : (P1 P2 LP2), num : N2 > < id(R3, C3) : cell | grd : G3, pss : LP3, At3 > < id(R4, C4) : cell | grd : G4, pss : LP4, At4 > < id(R5, C5) : cell | grd : G5, pss : LP5, At5 > < id(R6, C6) : cell | grd : G6, pss : LP6, At6 > < id(R7, C7) : cell | grd : G7, pss : LP7, At7 > < id(R8, C8) : cell | grd : G8, pss : LP8, At8 > < id(R9, C9) : cell | grd : G9, pss : LP9, At9 > => < id(R1, C1) : cell | grd : G1, pss : (P1 P2), num : 2 > < id(R2, C2) : cell | grd : G2, pss : (P1 P2), num : 2 > < id(R3, C3) : cell | grd : G3, pss : LP3, At3 > < id(R4, C4) : cell | grd : G4, pss : LP4, At4 > < id(R5, C5) : cell | grd : G5, pss : LP5, At5 > < id(R6, C6) : cell | grd : G6, pss : LP6, At6 > < id(R7, C7) : cell | grd : G7, pss : LP7, At7 > < id(R8, C8) : cell | grd : G8, pss : LP8, At8 > < id(R9, C9) : cell | grd : G9, pss : LP9, At9 > if (same(R1, R2, R3, R4, R5, R6, R7, R8, R9) or same(C1, C2, C3, C4, C5, C6, C7, C8, C9) or same(G1, G2, G3, G4, G5, G6, G7, G8, G9)) and disj((P1 P2), union(LP3, LP4, LP5, LP6, LP7, LP8, LP9)) . --- [twins] If, in a given grid, a number is only possible in one row (or --- column), then that number can be removed from the set of possible numbers --- in all the cells in that same row (or column) but different grid. crl [twins] : < id(R, C) : cell | grd : G', pss : (P LP), num : N > < id(R', C') : cell | grd : G, pss : (P LP'), num : N' > < id(R1, C1) : cell | grd : G, pss : LP1, At1 > < id(R2, C2) : cell | grd : G, pss : LP2, At2 > < id(R3, C3) : cell | grd : G, pss : LP3, At3 > < id(R4, C4) : cell | grd : G, pss : LP4, At4 > < id(R5, C5) : cell | grd : G, pss : LP5, At5 > < id(R6, C6) : cell | grd : G, pss : LP6, At6 > => < id(R, C) : cell | grd : G', pss : LP, num : sd(N, 1) > < id(R', C') : cell | grd : G, pss : (P LP'), num : N' > < id(R1, C1) : cell | grd : G, pss : LP1, At1 > < id(R2, C2) : cell | grd : G, pss : LP2, At2 > < id(R3, C3) : cell | grd : G, pss : LP3, At3 > < id(R4, C4) : cell | grd : G, pss : LP4, At4 > < id(R5, C5) : cell | grd : G, pss : LP5, At5 > < id(R6, C6) : cell | grd : G, pss : LP6, At6 > if (G =/= G') and not (P in union(LP1, LP2, LP3, LP4, LP5, LP6)) and ((same(R1, R2, R3) and same(R4, R5, R6)) or (same(C1, C2, C3) and same(C4, C5, C6))) . --- [sudokuSplit] This rule splits a sudoku when none of the other rules can --- be applied. We select a cell with a minimum number (greater than $1$) of --- possible numbers. Then a sudoku is created with the first possible number --- and another one with the remaining possible numbers. rl [sudokuSplit2] : << msg('SearchingSolution) VConf < id(R, C) : cell | grd : G, pss : (P1 P2), num : 2 > >> => << msg('SearchingSolution) VConf < id(R, C) : cell | grd : G, pss : P1, num : 1 > >> << msg('SearchingSolution) VConf < id(R, C) : cell | grd : G, pss : P2, num : 1 > >> . crl [sudokuSplitN] : << msg('SearchingSolution) VConf < id(R, C) : cell | grd : G, pss : (P LP), num : (s N) > >> => << msg('SearchingSolution) VConf < id(R, C) : cell | grd : G, pss : P, num : 1 > >> << msg('SearchingSolution) VConf < id(R, C) : cell | grd : G, pss : LP, num : N > >> if betCard(VConf < id(R, C) : cell | grd : G, pss : (P LP), num : (s N) >) == (s N) . --- [presentSolution] This equation presents the final solution of a sudoku. eq < id(R, 1) : cell | pss : N1, At1 > < id(R, 2) : cell | pss : N2, At2 > < id(R, 3) : cell | pss : N3, At3 > < id(R, 4) : cell | pss : N4, At4 > < id(R, 5) : cell | pss : N5, At5 > < id(R, 6) : cell | pss : N6, At6 > < id(R, 7) : cell | pss : N7, At7 > < id(R, 8) : cell | pss : N8, At8 > < id(R, 9) : cell | pss : N9, At9 > msg('FinalSolution) = < id(R, 0) : rows | val : (N1 ; N2 ; N3 ; N4 ; N5 ; N6 ; N7 ; N8 ; N9) > msg('FinalSolution) . --- This rule ends the procedure when all cells have a --- single possible number and presents a FinalSolution message. ceq << msg('SearchingSolution) VConf >> = << msg('FinalSolution) VConf >> if (maxCard(VConf) == 1) and (minCard(VConf) == 1) . eq << VMsg >> << msg('FinalSolution) VConf' >> = << msg('FinalSolution) VConf' >> . eq << VMsg VConf >> << msg('FinalSolution) VConf' >> = << msg('FinalSolution) VConf' >> . --- The procedure is stopped when a cell without possible numbers is found. eq << msg('SearchingSolution) VConf < id(R, C) : cell | pss : empty, At > >> = << msg('NoSolution) >> . endm) *** The strategies here are slightly different from the ones in the paper: *** they are a bit more efficient but slightly more cumbersome to describe. (stratdef STRAT is sop rulesA . seq rulesA = (simplify1st) . sop rulesB . seq rulesB = (simplify2nd orelse onlyOneNumber) . sop rulesC . seq rulesC = (onlyTwoNumbers orelse (simplify3rd orelse twins)) . sop split . seq split = sudokuSplit2 orelse sudokuSplitN . sop solve . seq solve = (rulesA orelse (rulesB orelse (rulesC orelse split))) ! . endsd) eof ---SUDOKU N01. Easy. The Daily Sudoku. Fri 21-Jan-2005 ( 0 ; 6 ; 2 ; 3 ; 4 ; 0 ; 7 ; 5 ; 0 ; 1 ; 0 ; 0 ; 0 ; 0 ; 5 ; 6 ; 0 ; 0 ; 5 ; 7 ; 0 ; 0 ; 0 ; 0 ; 0 ; 4 ; 0 ; 0 ; 0 ; 0 ; 0 ; 9 ; 4 ; 8 ; 0 ; 0 ; 4 ; 0 ; 0 ; 0 ; 0 ; 0 ; 0 ; 0 ; 6 ; 0 ; 0 ; 5 ; 8 ; 3 ; 0 ; 0 ; 0 ; 0 ; 0 ; 3 ; 0 ; 0 ; 0 ; 0 ; 0 ; 9 ; 1 ; 0 ; 0 ; 6 ; 4 ; 0 ; 0 ; 0 ; 0 ; 7 ; 0 ; 5 ; 9 ; 0 ; 8 ; 3 ; 2 ; 6 ; 0 ) ---SUDOKU N06. Medium. The Daily Sudoku. Wed 26-Jan-2005. ( 7 ; 8 ; 0 ; 9 ; 0 ; 2 ; 0 ; 0 ; 3 ; 0 ; 0 ; 0 ; 4 ; 0 ; 0 ; 0 ; 0 ; 0 ; 1 ; 3 ; 5 ; 0 ; 8 ; 0 ; 0 ; 0 ; 0 ; 0 ; 2 ; 0 ; 0 ; 1 ; 0 ; 0 ; 7 ; 8 ; 0 ; 0 ; 0 ; 0 ; 0 ; 0 ; 0 ; 0 ; 0 ; 6 ; 7 ; 0 ; 0 ; 9 ; 0 ; 0 ; 2 ; 0 ; 0 ; 0 ; 0 ; 0 ; 6 ; 0 ; 5 ; 9 ; 2 ; 0 ; 0 ; 0 ; 0 ; 0 ; 3 ; 0 ; 0 ; 0 ; 2 ; 0 ; 0 ; 5 ; 0 ; 9 ; 0 ; 6 ; 1 ) --- Diabolical sudoku. Crosswords Ltd, 2005 ( 0 ; 9 ; 0 ; 7 ; 0 ; 0 ; 8 ; 6 ; 0 ; 0 ; 3 ; 1 ; 0 ; 0 ; 5 ; 0 ; 2 ; 0 ; 8 ; 0 ; 6 ; 0 ; 0 ; 0 ; 0 ; 0 ; 0 ; 0 ; 0 ; 7 ; 0 ; 5 ; 0 ; 0 ; 0 ; 6 ; 0 ; 0 ; 0 ; 3 ; 0 ; 7 ; 0 ; 0 ; 0 ; 5 ; 0 ; 0 ; 0 ; 1 ; 0 ; 7 ; 0 ; 0 ; 0 ; 0 ; 0 ; 0 ; 0 ; 0 ; 1 ; 0 ; 9 ; 0 ; 2 ; 0 ; 6 ; 0 ; 0 ; 3 ; 5 ; 0 ; 0 ; 5 ; 4 ; 0 ; 0 ; 8 ; 0 ; 7 ; 0 )