(role player)

; Initial state.
(init (cell 1 1 b))
(init (cell 2 1 1))
(init (cell 3 1 4))
(init (cell 4 1 3))
(init (cell 5 1 5))
(init (cell 6 1 9))
(init (cell 7 1 2))
(init (cell 8 1 6))
(init (cell 9 1 b))

(init (cell 1 2 5))
(init (cell 2 2 b))
(init (cell 3 2 2))
(init (cell 4 2 1))
(init (cell 5 2 b))
(init (cell 6 2 6))
(init (cell 7 2 3))
(init (cell 8 2 b))
(init (cell 9 2 8))

(init (cell 1 3 9))
(init (cell 2 3 3))
(init (cell 3 3 b))
(init (cell 4 3 8))
(init (cell 5 3 7))
(init (cell 6 3 2))
(init (cell 7 3 b))
(init (cell 8 3 1))
(init (cell 9 3 5))

(init (cell 1 4 7))
(init (cell 2 4 6))
(init (cell 3 4 5))
(init (cell 4 4 b))
(init (cell 5 4 3))
(init (cell 6 4 b))
(init (cell 7 4 9))
(init (cell 8 4 2))
(init (cell 9 4 1))

(init (cell 1 5 b))
(init (cell 2 5 8))
(init (cell 3 5 1))
(init (cell 4 5 9))
(init (cell 5 5 b))
(init (cell 6 5 7))
(init (cell 7 5 6))
(init (cell 8 5 5))
(init (cell 9 5 b))

(init (cell 1 6 2))
(init (cell 2 6 4))
(init (cell 3 6 9))
(init (cell 4 6 b))
(init (cell 5 6 1))
(init (cell 6 6 b))
(init (cell 7 6 8))
(init (cell 8 6 7))
(init (cell 9 6 3))

(init (cell 1 7 6))
(init (cell 2 7 2))
(init (cell 3 7 b))
(init (cell 4 7 7))
(init (cell 5 7 8))
(init (cell 6 7 1))
(init (cell 7 7 b))
(init (cell 8 7 4))
(init (cell 9 7 9))

(init (cell 1 8 1))
(init (cell 2 8 b))
(init (cell 3 8 8))
(init (cell 4 8 5))
(init (cell 5 8 b))
(init (cell 6 8 4))
(init (cell 7 8 7))
(init (cell 8 8 b))
(init (cell 9 8 2))

(init (cell 1 9 b))
(init (cell 2 9 5))
(init (cell 3 9 7))
(init (cell 4 9 2))
(init (cell 5 9 9))
(init (cell 6 9 3))
(init (cell 7 9 1))
(init (cell 8 9 8))
(init (cell 9 9 b))

; Group membership.
(<= (member (cell ?x ?y) (column ?x))
    (dig ?x)
    (dig ?y))
(<= (member (cell ?x ?y) (row ?y))
    (dig ?x)
    (dig ?y))
(major 1 low)
(major 2 low)
(major 3 low)
(major 4 middle)
(major 5 middle)
(major 6 middle)
(major 7 high)
(major 8 high)
(major 9 high)
(<= (member (cell ?x ?y) (box ?major_col ?major_row))
    (major ?x ?major_col)
    (major ?y ?major_row))

; Successor axioms
(succ 0 1)
(succ 1 2)
(succ 2 3)
(succ 3 4)
(succ 4 5)
(succ 5 6)
(succ 6 7)
(succ 7 8)
(succ 8 9)
(succ 9 10)
(succ 10 11)
(succ 11 12)
(succ 12 13)
(succ 13 14)
(succ 14 15)
(succ 15 16)
(succ 16 17)
(succ 17 18)
(succ 18 19)
(succ 19 20)
(succ 20 21)
(succ 21 22)
(succ 22 23)
(succ 23 24)
(succ 24 25)
(succ 25 26)
(succ 26 27)

(dig 1)
(dig 2)
(dig 3)
(dig 4)
(dig 5)
(dig 6)
(dig 7)
(dig 8)
(dig 9)

; Legal moves
(<= (legal player (write ?x ?y ?value))
    (true (cell ?x ?y b))
    (dig ?value))

; Scoring: 3 points for each column, row, and box that is complete.
; Add 19 if puzzle is completed, so 100 is top score.
(score 0 0)
(score 1 3)
(score 2 6)
(score 3 9)
(score 4 12)
(score 5 15)
(score 6 18)
(score 7 21)
(score 8 24)
(score 9 27)
(score 10 30)
(score 11 33)
(score 12 36)
(score 13 39)
(score 14 42)
(score 15 45)
(score 16 48)
(score 17 51)
(score 18 54)
(score 19 57)
(score 20 60)
(score 21 63)
(score 22 66)
(score 23 69)
(score 24 72)
(score 25 75)
(score 26 78)
(score 27 100)

(<= (goal player ?g)
    (total ?t)
    (score ?t ?g))

(<= (total ?n)
    (count (box high high) ?n))

(box_position high)
(box_position middle)
(box_position low)
(<= (group (box ?x ?y))
    (box_position ?x)
    (box_position ?y))
(<= (group (row ?x))
    (dig ?x))
(<= (group (column ?x))
    (dig ?x))

(next_group (box high middle) (box high high))
(next_group (box high low) (box high middle))
(next_group (box middle high) (box high low))
(next_group (box middle middle) (box middle high))
(next_group (box middle low) (box middle middle))
(next_group (box low high) (box middle low))
(next_group (box low middle) (box low high))
(next_group (box low low) (box low middle))
(next_group (row 9) (box low low))
(next_group (column 9) (row 1)) 
(<= (next_group (box ?a) (box ?b))
    (succ ?a ?b)
    (dig ?a)
    (dig ?b))
(<= (next_group (column ?a) (column ?b))
    (succ ?a ?b)
    (dig ?a)
    (dig ?b))
(<= (next_group (row ?a) (row ?b))
    (succ ?a ?b)
    (dig ?a)
    (dig ?b))

(<= (count (column 1) 0)
    (not (complete (column 1))))

(<= (count (column 1) 1)
    (complete (column 1)))
(<= (count ?g2 ?p)
    (group ?g2)
    (not (complete ?g2))
    (next_group ?g1 ?g2)
    (count ?g1 ?p))
(<= (count ?g2 ?p2)
    (complete ?g2)
    (next_group ?g1 ?g2)
    (count ?g1 ?p1)
    (succ ?p1 ?p2))

(<= (complete ?group)
    (contains ?group 1)
    (contains ?group 2)
    (contains ?group 3)
    (contains ?group 4)
    (contains ?group 5)
    (contains ?group 6)
    (contains ?group 7)
    (contains ?group 8)
    (contains ?group 9))

(<= (contains ?group ?digit)
    (member (cell ?x ?y) ?group)
    (true (cell ?x ?y ?digit)))

; Transition rules
(<= (next (cell ?x ?y ?value))
    (does player (write ?x ?y ?value)))
(<= (next (cell ?x ?y ?value))
    (true (cell ?x ?y ?value))
    (does player (write ?x2 ?y2 ?anything))
    (distinct ?x ?x2))
(<= (next (cell ?x ?y ?value))
    (true (cell ?x ?y ?value))
    (does player (write ?x2 ?y2 ?anything))
    (distinct ?y ?y2))

; Termination
(<= terminal 
  (not (true (cell 1 1 b)))
  (not (true (cell 9 1 b)))
  (not (true (cell 2 2 b)))
  (not (true (cell 5 2 b)))
  (not (true (cell 8 2 b)))
  (not (true (cell 3 3 b)))
  (not (true (cell 7 3 b)))
  (not (true (cell 4 4 b)))
  (not (true (cell 6 4 b)))
  (not (true (cell 1 5 b)))
  (not (true (cell 5 5 b)))
  (not (true (cell 9 5 b)))
  (not (true (cell 4 6 b)))
  (not (true (cell 6 6 b)))
  (not (true (cell 3 7 b)))
  (not (true (cell 7 7 b)))
  (not (true (cell 2 8 b)))
  (not (true (cell 5 8 b)))
  (not (true (cell 8 8 b)))
  (not (true (cell 1 9 b)))
  (not (true (cell 9 9 b))))