;;
;; Sudoku example. xij denotes what's at line i, column j
;; 

(set-param var-elim true)
(set-param arith-elim true)
(set-param flatten true)
(set-param simplex-prop true)
(set-param branching default)

(define x11::int)
(define x12::int)
(define x13::int)
(define x14::int)
(define x15::int)
(define x16::int)
(define x17::int)
(define x18::int)
(define x19::int)

(define x21::int)
(define x22::int)
(define x23::int)
(define x24::int)
(define x25::int)
(define x26::int)
(define x27::int)
(define x28::int)
(define x29::int)

(define x31::int)
(define x32::int)
(define x33::int)
(define x34::int)
(define x35::int)
(define x36::int)
(define x37::int)
(define x38::int)
(define x39::int)

(define x41::int)
(define x42::int)
(define x43::int)
(define x44::int)
(define x45::int)
(define x46::int)
(define x47::int)
(define x48::int)
(define x49::int)

(define x51::int)
(define x52::int)
(define x53::int)
(define x54::int)
(define x55::int)
(define x56::int)
(define x57::int)
(define x58::int)
(define x59::int)

(define x61::int)
(define x62::int)
(define x63::int)
(define x64::int)
(define x65::int)
(define x66::int)
(define x67::int)
(define x68::int)
(define x69::int)

(define x71::int)
(define x72::int)
(define x73::int)
(define x74::int)
(define x75::int)
(define x76::int)
(define x77::int)
(define x78::int)
(define x79::int)

(define x81::int)
(define x82::int)
(define x83::int)
(define x84::int)
(define x85::int)
(define x86::int)
(define x87::int)
(define x88::int)
(define x89::int)

(define x91::int)
(define x92::int)
(define x93::int)
(define x94::int)
(define x95::int)
(define x96::int)
(define x97::int)
(define x98::int)
(define x99::int)


(assert 
  (and (= x11 1) (= x21 2) (= x31 3) (= x41 4)
       (= x51 5) (= x61 6) (= x71 7) (= x81 8) (= x91 9)))

(assert 
  (and (<= 1 x11) (<= x11 9)
       (<= 1 x12) (<= x12 9)
       (<= 1 x13) (<= x13 9)
       (<= 1 x14) (<= x14 9)
       (<= 1 x15) (<= x15 9)
       (<= 1 x16) (<= x16 9)
       (<= 1 x17) (<= x17 9)
       (<= 1 x18) (<= x18 9)
       (<= 1 x19) (<= x19 9)

       (<= 1 x21) (<= x21 9) 
       (<= 1 x22) (<= x22 9)
       (<= 1 x23) (<= x23 9)
       (<= 1 x24) (<= x24 9)
       (<= 1 x25) (<= x25 9)
       (<= 1 x26) (<= x26 9)
       (<= 1 x27) (<= x27 9)
       (<= 1 x28) (<= x28 9)
       (<= 1 x29) (<= x29 9)

       (<= 1 x31) (<= x31 9) 
       (<= 1 x32) (<= x32 9)
       (<= 1 x33) (<= x33 9)
       (<= 1 x34) (<= x34 9)
       (<= 1 x35) (<= x35 9)
       (<= 1 x36) (<= x36 9)
       (<= 1 x37) (<= x37 9)
       (<= 1 x38) (<= x38 9)
       (<= 1 x39) (<= x39 9)

       (<= 1 x41) (<= x41 9) 
       (<= 1 x42) (<= x42 9)
       (<= 1 x43) (<= x43 9)
       (<= 1 x44) (<= x44 9)
       (<= 1 x45) (<= x45 9)
       (<= 1 x46) (<= x46 9)
       (<= 1 x47) (<= x47 9)
       (<= 1 x48) (<= x48 9)
       (<= 1 x49) (<= x49 9)

       (<= 1 x51) (<= x51 9) 
       (<= 1 x52) (<= x52 9)
       (<= 1 x53) (<= x53 9)
       (<= 1 x54) (<= x54 9)
       (<= 1 x55) (<= x55 9)
       (<= 1 x56) (<= x56 9)
       (<= 1 x57) (<= x57 9)
       (<= 1 x58) (<= x58 9)
       (<= 1 x59) (<= x59 9)

       (<= 1 x61) (<= x61 9) 
       (<= 1 x62) (<= x62 9)
       (<= 1 x63) (<= x63 9)
       (<= 1 x64) (<= x64 9)
       (<= 1 x65) (<= x65 9)
       (<= 1 x66) (<= x66 9)
       (<= 1 x67) (<= x67 9)
       (<= 1 x68) (<= x68 9)
       (<= 1 x69) (<= x69 9)

       (<= 1 x71) (<= x71 9) 
       (<= 1 x72) (<= x72 9)
       (<= 1 x73) (<= x73 9)
       (<= 1 x74) (<= x74 9)
       (<= 1 x75) (<= x75 9)
       (<= 1 x76) (<= x76 9)
       (<= 1 x77) (<= x77 9)
       (<= 1 x78) (<= x78 9)
       (<= 1 x79) (<= x79 9)

       (<= 1 x81) (<= x81 9) 
       (<= 1 x82) (<= x82 9)
       (<= 1 x83) (<= x83 9)
       (<= 1 x84) (<= x84 9)
       (<= 1 x85) (<= x85 9)
       (<= 1 x86) (<= x86 9)
       (<= 1 x87) (<= x87 9)
       (<= 1 x88) (<= x88 9)
       (<= 1 x89) (<= x89 9)

       (<= 1 x91) (<= x91 9) 
       (<= 1 x92) (<= x92 9)
       (<= 1 x93) (<= x93 9)
       (<= 1 x94) (<= x94 9)
       (<= 1 x95) (<= x95 9)
       (<= 1 x96) (<= x96 9)
       (<= 1 x97) (<= x97 9)
       (<= 1 x98) (<= x98 9)
       (<= 1 x99) (<= x99 9)))



(assert (distinct x11 x12 x13 x14 x15 x16 x17 x18 x19))
(assert (distinct x21 x22 x23 x24 x25 x26 x27 x28 x29))
(assert (distinct x31 x32 x33 x34 x35 x36 x37 x38 x39))
(assert (distinct x41 x42 x43 x44 x45 x46 x47 x48 x49))
(assert (distinct x51 x52 x53 x54 x55 x56 x57 x58 x59))
(assert (distinct x61 x62 x63 x64 x65 x66 x67 x68 x69))
(assert (distinct x71 x72 x73 x74 x75 x76 x77 x78 x79))
(assert (distinct x81 x82 x83 x84 x85 x86 x87 x88 x89))
(assert (distinct x91 x92 x93 x94 x95 x96 x97 x98 x99))

(assert (distinct x11 x21 x31 x41 x51 x61 x71 x81 x91))
(assert (distinct x12 x22 x32 x42 x52 x62 x72 x82 x92))
(assert (distinct x13 x23 x33 x43 x53 x63 x73 x83 x93))
(assert (distinct x14 x24 x34 x44 x54 x64 x74 x84 x94))
(assert (distinct x15 x25 x35 x45 x55 x65 x75 x85 x95))
(assert (distinct x16 x26 x36 x46 x56 x66 x76 x86 x96))
(assert (distinct x17 x27 x37 x47 x57 x67 x77 x87 x97))
(assert (distinct x18 x28 x38 x48 x58 x68 x78 x88 x98))
(assert (distinct x19 x29 x39 x49 x59 x69 x79 x89 x99))

(assert (distinct x11 x12 x13 x21 x22 x23 x31 x32 x33))
(assert (distinct x14 x15 x16 x24 x25 x26 x34 x35 x36))
(assert (distinct x17 x18 x19 x27 x28 x29 x37 x38 x39))

(assert (distinct x41 x42 x43 x51 x52 x53 x61 x62 x63))
(assert (distinct x44 x45 x46 x54 x55 x56 x64 x65 x66))
(assert (distinct x47 x48 x49 x57 x58 x59 x67 x68 x69))

(assert (distinct x71 x72 x73 x81 x82 x83 x91 x92 x93))
(assert (distinct x74 x75 x76 x84 x85 x86 x94 x95 x96))
(assert (distinct x77 x78 x79 x87 x88 x89 x97 x98 x99))

(check)

(show-model)