constraint solver solution for https://fosstodon.org/@ianthetechie/114347924920243335 use e.g. z3

puzzle.smt2

(set-logic QF_LIA)

; x0 x1 x2
; x3 x4 x5
; x6 x7 x8

(declare-const x0 Int)
(declare-const x1 Int)
(declare-const x2 Int)
(declare-const x3 Int)
(declare-const x4 Int)
(declare-const x5 Int)
(declare-const x6 Int)
(declare-const x7 Int)
(declare-const x8 Int)

(assert (>= x0 0))
(assert (>= x1 0))
(assert (>= x2 0))
(assert (>= x3 0))
(assert (>= x4 0))
(assert (>= x5 0))
(assert (>= x6 0))
(assert (>= x7 0))
(assert (>= x8 0))

; consecutive numbers constraint

(assert (distinct x1 x2 x3 x4 x5 x6 x7 x8))

(define-fun max ((x Int) (y Int)) Int
  (ite (> x y) x y))

(define-fun min ((x Int) (y Int)) Int
  (ite (< x y) x y))

(assert
  (= 8
    (-
      (max x0 (max x1 (max x2 (max x3 (max x4 (max x5 (max x6 (max x7 x8))))))))
      (min x0 (min x1 (min x2 (min x3 (min x4 (min x5 (min x6 (min x7 x8)))))))))))

; rows sum up to 60

(assert (= 60 (+ x0 x1 x2)))
(assert (= 60 (+ x3 x4 x5)))
(assert (= 60 (+ x6 x7 x8)))

; cols sum up to 60

(assert (= 60 (+ x0 x3 x6)))
(assert (= 60 (+ x1 x4 x7)))
(assert (= 60 (+ x2 x5 x8)))

; diags sum up to 60

(assert (= 60 (+ x0 x4 x8)))
(assert (= 60 (+ x6 x4 x2)))

; solve

(check-sat)
(get-model)
(exit)

$ z3 solve.smt2
sat

(
  (define-fun x4 () Int
    20)
  (define-fun x1 () Int
    16)
  (define-fun x2 () Int
    21)
  (define-fun x0 () Int
    23)
  (define-fun x3 () Int
    18)
  (define-fun x7 () Int
    24)
  (define-fun x6 () Int
    19)
  (define-fun x5 () Int
    22)
  (define-fun x8 () Int
    17)
)