(mod SUDOKU is 
  protecting NAT .  
  protecting QID .  
  protecting CONVERSION .

--- Description. Sudoku Monster Solver with Strategies

--- Same rules 16x16 table (4x4 grids) with 0 to 16 numbers.
--- Author: Gustavo Santos-Garcia & Miguel Palomino

--- email: santos@usal.es, miguelpt@sip.ucm.es

--- Date. Feb 10, 2006

--- Version: 1.0.0

*** 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,
(  1 ;  0 ;  4 ;  9 ;     0 ;  0 ;  5 ; 11 ;     3 ; 14 ;  0 ;  0 ;    10 ;  0 ; 15 ;  0 ;

   7 ;  0 ;  0 ;  0 ;     0 ;  0 ;  0 ;  0 ;     1 ;  0 ;  2 ; 16 ;     0 ;  0 ;  0 ;  0 ;

  14 ;  2 ;  0 ; 11 ;     0 ;  0 ; 10 ;  0 ;     0 ;  0 ;  0 ;  0 ;     0 ;  9 ;  0 ; 12 ;

   3 ;  8 ;  5 ;  0 ;     0 ; 14 ;  0 ;  1 ;     0 ; 10 ;  0 ;  4 ;     7 ;  0 ;  6 ; 13 ;

---
   0 ;  0 ;  8 ;  0 ;     9 ;  6 ; 11 ;  0 ;     0 ;  2 ;  4 ;  3 ;     0 ;  0 ;  0 ; 10 ;

   0 ;  0 ; 14 ;  0 ;     0 ;  0 ;  0 ;  0 ;     0 ;  8 ;  0 ;  0 ;     3 ;  0 ;  0 ;  0 ;

   0 ;  0 ;  1 ;  0 ;     3 ;  4 ;  0 ;  5 ;    14 ;  0 ;  0 ; 15 ;    11 ;  0 ;  0 ;  0 ;

   6 ;  5 ; 10 ;  0 ;    12 ;  0 ;  2 ;  8 ;     0 ; 11 ;  0 ;  0 ;     0 ;  4 ;  0 ;  9 ;

---
   9 ;  0 ;  6 ;  0 ;     0 ;  0 ;  3 ;  0 ;     4 ;  7 ;  0 ; 10 ;     0 ; 12 ;  2 ;  5 ;

   0 ;  0 ;  0 ;  2 ;     6 ;  0 ;  0 ; 13 ;     9 ;  0 ;  5 ;  8 ;     0 ; 10 ;  0 ;  0 ;

   0 ;  0 ;  0 ; 16 ;     0 ;  0 ;  1 ;  0 ;     0 ;  0 ;  0 ;  0 ;     0 ;  3 ;  0 ;  0 ;

   8 ;  0 ;  0 ;  0 ;    16 ;  7 ;  4 ;  0 ;     0 ;  1 ; 11 ;  2 ;     0 ; 14 ;  0 ;  0 ;

---
  13 ;  7 ;  0 ;  1 ;     5 ;  0 ;  8 ;  0 ;    10 ;  0 ; 15 ;  0 ;     0 ; 16 ; 12 ; 14 ;

  16 ;  0 ;  9 ;  0 ;     0 ;  0 ;  0 ;  0 ;     0 ;  5 ;  0 ;  0 ;    15 ;  0 ; 13 ;  3 ;

  12 ; 14 ;  3 ;  8 ;    13 ;  1 ; 15 ;  4 ;     2 ; 16 ;  7 ; 11 ;     9 ;  5 ; 10 ;  6 ;
   5 ; 10 ;  2 ; 15 ;    14 ; 16 ;  6 ;  7 ;    12 ; 13 ;  3 ;  9 ;     4 ;  1 ;  8 ; 11 )

           ) >> .

  op fill : Nat Nat List -> Object .   
  eq  fill( R, C, (N ; LL)) =   
      if C == 16 then   --- 16 is the number of cells in a row
        < 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 4) * 4  +  (sd(C, 1) quo 4) + 1 . --- 4 instead of 3

  op pss : Nat -> Set .  
  eq pss(N) =    --- and 10 ... 16
     if N == 0 then (1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16) else (N) fi .  

  op num : Nat -> Nat . 
  eq num(N) = if N == 0 then 16 else 1 fi .  --- 16 instead of 9


********* 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 At10 At11 At12 At13 At14 At15 At16 : AttributeSet .
  vars N N' N1 N2 N3 N4 N5 N6 N7 N8 N9 N10 N11 N12 N13 N14 N15 N16   R R' R1 R2 R3 R4 R5 R6 R7 R8 R9 R10 R11 R12 R13 R14 R15 R16 : Nat . 
  vars C C' C1 C2 C3 C4 C5 C6 C7 C8 C9 C10 C11 C12 C13 C14 C15 C16   G G' G1 G2 G3 G4 G5 G6 G7 G8 G9 G10 G11 G12 G13 G14 G15 G16   P P' P1 P2 P3 P4 : Nat . 
  vars LP LP' LP1 LP2 LP3 LP4 LP5 LP6 LP7 LP8 LP9 LP10 LP11 LP12 LP13 LP14 LP15 LP16 : 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 .
  op same : Nat Nat Nat Nat Nat Nat Nat 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)) .
  eq same(R1, R2, R3, R4, R5, R6, R7, R8, R9, R10, R11, R12, R13, R14, R15, R16) = 
     ((R1 == R2) and (R1 == R3) and (R1 == R4) and (R1 == R5) and 
      (R1 == R6) and (R1 == R7) and (R1 == R8) and (R1 == R9) and
      (R1 == R10) and (R1 == R11) and (R1 == R12) and (R1 == R13) and 
      (R1 == R14) and (R1 == R15) and (R1 == R16)) .

********* 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(R10, C10) : cell  | grd : G10, pss : LP10, At10 > 
    < id(R11, C11) : cell  | grd : G11, pss : LP11, At11 > 
    < id(R12, C12) : cell  | grd : G12, pss : LP12, At12 > 
    < id(R13, C13) : cell  | grd : G13, pss : LP13, At13 > 
    < id(R14, C14) : cell  | grd : G14, pss : LP14, At14 > 
    < id(R15, C15) : cell  | grd : G15, pss : LP15, At15 > 
    < id(R16, C16) : cell  | grd : G16, pss : LP16, At16 > 
=>  < 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 > 
    < id(R10, C10) : cell  | grd : G10, pss : LP10, At10 > 
    < id(R11, C11) : cell  | grd : G11, pss : LP11, At11 > 
    < id(R12, C12) : cell  | grd : G12, pss : LP12, At12 > 
    < id(R13, C13) : cell  | grd : G13, pss : LP13, At13 > 
    < id(R14, C14) : cell  | grd : G14, pss : LP14, At14 > 
    < id(R15, C15) : cell  | grd : G15, pss : LP15, At15 > 
    < id(R16, C16) : cell  | grd : G16, pss : LP16, At16 > 
  if (same(R1, R2, R3, R4, R5, R6, R7, R8, R9, R10, R11, R12, R13, R14, R15, R16) or 
      same(C1, C2, C3, C4, C5, C6, C7, C8, C9, C10, C11, C12, C13, C14, C15, C16) or 
      same(G1, G2, G3, G4, G5, G6, G7, G8, G9, G10, G11, G12, G13, G14, G15, G16)) and
      not (P in union(LP2, LP3, LP4, LP5, LP6, LP7, LP8, LP9, LP10, LP11, LP12, LP13, LP14, LP15, LP16)) .

  --- [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(R10, C10) : cell  | grd : G10, pss : LP10, At10 > 
      < id(R11, C11) : cell  | grd : G11, pss : LP11, At11 > 
      < id(R12, C12) : cell  | grd : G12, pss : LP12, At12 > 
      < id(R13, C13) : cell  | grd : G13, pss : LP13, At13 > 
      < id(R14, C14) : cell  | grd : G14, pss : LP14, At14 > 
      < id(R15, C15) : cell  | grd : G15, pss : LP15, At15 > 
      < id(R16, C16) : cell  | grd : G16, pss : LP16, At16 > 
  =>  < 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 > 
      < id(R10, C10) : cell  | grd : G10, pss : LP10, At10 > 
      < id(R11, C11) : cell  | grd : G11, pss : LP11, At11 > 
      < id(R12, C12) : cell  | grd : G12, pss : LP12, At12 > 
      < id(R13, C13) : cell  | grd : G13, pss : LP13, At13 > 
      < id(R14, C14) : cell  | grd : G14, pss : LP14, At14 > 
      < id(R15, C15) : cell  | grd : G15, pss : LP15, At15 > 
      < id(R16, C16) : cell  | grd : G16, pss : LP16, At16 > 
  if (same(R1, R2, R3, R4, R5, R6, R7, R8, R9, R10, R11, R12, R13, R14, R15, R16) or 
    same(C1, C2, C3, C4, C5, C6, C7, C8, C9, C10, C11, C12, C13, C14, C15, C16) or 
    same(G1, G2, G3, G4, G5, G6, G7, G8, G9, G10, G11, G12, G13, G14, G15, G16))    and
    disj((P1 P2), union(LP3, LP4, LP5, LP6, LP7, LP8, LP9, LP10, LP11, LP12, LP13, LP14, LP15, LP16)) .

  --- [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(R7, C7) : cell  | grd : G, pss : LP7, At7 >
      < id(R8, C8) : cell  | grd : G, pss : LP8, At8 >
  =>  < 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 >
      < id(R7, C7) : cell  | grd : G, pss : LP7, At7 >
      < id(R8, C8) : cell  | grd : G, pss : LP8, At8 >
  if (G =/= G') and  not (P in union(LP1, LP2, LP3, LP4, LP5, LP6, LP7, LP8)) and
     ((same(R1, R2, R3, R4) and  same(R5, R6, R7, R8)) or   
      (same(C1, C2, C3, C4) and  same(C5, C6, C7, C8))) .

  --- [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 >  < id(R, 10) : cell | pss : N10, At10 >  
     < id(R, 11) : cell | pss : N11, At11 >  < id(R, 12) : cell | pss : N12, At12 >
     < id(R, 13) : cell | pss : N13, At13 >  < id(R, 14) : cell | pss : N14, At14 >
     < id(R, 15) : cell  | pss : N15, At15 > < id(R, 16) : cell | pss : N16, At16 >    
     msg('FinalSolution) 
    =   
     < id(R, 0) : rows | val : (N1 ; N2 ; N3 ; N4 ; N5 ; N6 ; N7 ; N8 ; N9 ; N10 ; N11 ; N12 ; N13 ; N14 ; N15 ; N16) >  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' >> .
  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-MONSTER N01. Difficulty rating: 2/5
--- No. SG0001 Compiled by D. Bodycombe Distribution www.knightfeatures.com
--- A->10, B->11, C->12, D->13, E->14, F->15 and 0->16

(  1 ;  0 ;  4 ;  9 ;     0 ;  0 ;  5 ; 11 ;     3 ; 14 ;  0 ;  0 ;    10 ;  0 ; 15 ;  0 ;

   7 ;  0 ;  0 ;  0 ;     0 ;  0 ;  0 ;  0 ;     1 ;  0 ;  2 ; 16 ;     0 ;  0 ;  0 ;  0 ;

  14 ;  2 ;  0 ; 11 ;     0 ;  0 ; 10 ;  0 ;     0 ;  0 ;  0 ;  0 ;     0 ;  9 ;  0 ; 12 ;

   3 ;  8 ;  5 ;  0 ;     0 ; 14 ;  0 ;  1 ;     0 ; 10 ;  0 ;  4 ;     7 ;  0 ;  6 ; 13 ;

---
   0 ;  0 ;  8 ;  0 ;     9 ;  6 ; 11 ;  0 ;     0 ;  2 ;  4 ;  3 ;     0 ;  0 ;  0 ; 10 ;

   0 ;  0 ; 14 ;  0 ;     0 ;  0 ;  0 ;  0 ;     0 ;  8 ;  0 ;  0 ;     3 ;  0 ;  0 ;  0 ;

   0 ;  0 ;  1 ;  0 ;     3 ;  4 ;  0 ;  5 ;    14 ;  0 ;  0 ; 15 ;    11 ;  0 ;  0 ;  0 ;

   6 ;  5 ; 10 ;  0 ;    12 ;  0 ;  2 ;  8 ;     0 ; 11 ;  0 ;  0 ;     0 ;  4 ;  0 ;  9 ;

---
   9 ;  0 ;  6 ;  0 ;     0 ;  0 ;  3 ;  0 ;     4 ;  7 ;  0 ; 10 ;     0 ; 12 ;  2 ;  5 ;

   0 ;  0 ;  0 ;  2 ;     6 ;  0 ;  0 ; 13 ;     9 ;  0 ;  5 ;  8 ;     0 ; 10 ;  0 ;  0 ;

   0 ;  0 ;  0 ; 16 ;     0 ;  0 ;  1 ;  0 ;     0 ;  0 ;  0 ;  0 ;     0 ;  3 ;  0 ;  0 ;

   8 ;  0 ;  0 ;  0 ;    16 ;  7 ;  4 ;  0 ;     0 ;  1 ; 11 ;  2 ;     0 ; 14 ;  0 ;  0 ;

---
  13 ;  7 ;  0 ;  1 ;     5 ;  0 ;  8 ;  0 ;    10 ;  0 ; 15 ;  0 ;     0 ; 16 ; 12 ; 14 ;

  16 ;  0 ;  9 ;  0 ;     0 ;  0 ;  0 ;  0 ;     0 ;  5 ;  0 ;  0 ;    15 ;  0 ; 13 ;  3 ;

   0 ;  0 ;  0 ;  0 ;    13 ;  1 ;  0 ;  4 ;     0 ;  0 ;  0 ;  0 ;     0 ;  0 ;  0 ;  6 ;

   0 ; 10 ;  0 ; 15 ;     0 ;  0 ;  6 ;  7 ;    12 ; 13 ;  0 ;  0 ;     4 ;  1 ;  0 ; 11 )


