BOJ 17106 Solution

boj17106.smt2

; BOJ 17106 Solution
; © 2025 Jinoh Kang. All rights reserved.

(set-option :produce-unsat-cores true)
(set-option :produce-models true)
(set-logic QF_LIA)

(declare-const A1 Bool)
(declare-const A2 Bool)
(declare-const A3 Bool)
(declare-const A4 Bool)
(declare-const A5 Bool)
(declare-const B1 Bool)
(declare-const B2 Bool)
(declare-const B3 Bool)
(declare-const B4 Bool)
(declare-const B5 Bool)
(declare-const C1 Bool)
(declare-const C2 Bool)
(declare-const C3 Bool)
(declare-const C4 Bool)
(declare-const C5 Bool)
(declare-const D1 Bool)
(declare-const D2 Bool)
(declare-const D3 Bool)
(declare-const D4 Bool)
(declare-const D5 Bool)
(declare-const E1 Bool)
(declare-const E2 Bool)
(declare-const E3 Bool)
(declare-const E4 Bool)
(declare-const E5 Bool)

(define-const A_ Bool (and A1 A2 A3 A4 A5))
(define-const B_ Bool (and B1 B2 B3 B4 B5))
(define-const C_ Bool (and C1 C2 C3 C4 C5))
(define-const D_ Bool (and D1 D2 D3 D4 D5))
(define-const E_ Bool (and E1 E2 E3 E4 E5))
(define-const anycol Bool (or A_ B_ C_ D_ E_))
(define-const numcol Int (+ (ite A_ 1 0) (ite B_ 1 0) (ite C_ 1 0) (ite D_ 1 0) (ite E_ 1 0)))

(define-const _1 Bool (and A1 B1 C1 D1 E1))
(define-const _2 Bool (and A2 B2 C2 D2 E2))
(define-const _3 Bool (and A3 B3 C3 D3 E3))
(define-const _4 Bool (and A4 B4 C4 D4 E4))
(define-const _5 Bool (and A5 B5 C5 D5 E5))
(define-const anyrow Bool (or _1 _2 _3 _4 _5))
(define-const numrow Int (+ (ite _1 1 0) (ite _2 1 0) (ite _3 1 0) (ite _4 1 0) (ite _5 1 0)))

(define-const A1E5 Bool (and A1 B2 C3 D4 E5))
(define-const A5E1 Bool (and A5 B4 C3 D2 E1))
(define-const anydiag Bool (or A1E5 A5E1))
(define-const numdiag Int (+ (ite A1E5 1 0) (ite A5E1 1 0)))

(define-const numb Int (+ numcol numrow numdiag))

(define-const A1b Bool (or A_ _1 A1E5))
(define-const A2b Bool (or A_ _2))
(define-const A3b Bool (or A_ _3))
(define-const A4b Bool (or A_ _4))
(define-const A5b Bool (or A_ _5 A5E1))
(define-const B1b Bool (or B_ _1))
(define-const B2b Bool (or B_ _2 A1E5))
(define-const B3b Bool (or B_ _3))
(define-const B4b Bool (or B_ _4 A5E1))
(define-const B5b Bool (or B_ _5))
(define-const C1b Bool (or C_ _1))
(define-const C2b Bool (or C_ _2))
(define-const C3b Bool (or C_ _3 A1E5 A5E1))
(define-const C4b Bool (or C_ _4))
(define-const C5b Bool (or C_ _5))
(define-const D1b Bool (or D_ _1))
(define-const D2b Bool (or D_ _2 A5E1))
(define-const D3b Bool (or D_ _3))
(define-const D4b Bool (or D_ _4 A1E5))
(define-const D5b Bool (or D_ _5))
(define-const E1b Bool (or E_ _1 A5E1))
(define-const E2b Bool (or E_ _2))
(define-const E3b Bool (or E_ _3))
(define-const E4b Bool (or E_ _4))
(define-const E5b Bool (or E_ _5 A1E5))

(define-const A1i Int (ite A1 1 0))
(define-const A2i Int (ite A2 1 0))
(define-const A3i Int (ite A3 1 0))
(define-const A4i Int (ite A4 1 0))
(define-const A5i Int (ite A5 1 0))
(define-const B1i Int (ite B1 1 0))
(define-const B2i Int (ite B2 1 0))
(define-const B3i Int (ite B3 1 0))
(define-const B4i Int (ite B4 1 0))
(define-const B5i Int (ite B5 1 0))
(define-const C1i Int (ite C1 1 0))
(define-const C2i Int (ite C2 1 0))
(define-const C3i Int (ite C3 1 0))
(define-const C4i Int (ite C4 1 0))
(define-const C5i Int (ite C5 1 0))
(define-const D1i Int (ite D1 1 0))
(define-const D2i Int (ite D2 1 0))
(define-const D3i Int (ite D3 1 0))
(define-const D4i Int (ite D4 1 0))
(define-const D5i Int (ite D5 1 0))
(define-const E1i Int (ite E1 1 0))
(define-const E2i Int (ite E2 1 0))
(define-const E3i Int (ite E3 1 0))
(define-const E4i Int (ite E4 1 0))
(define-const E5i Int (ite E5 1 0))

(define-const npb Int (+ (ite (and A1 A1b) 1 0)
                         (ite (and A2 A2b) 1 0)
                         (ite (and A3 A3b) 1 0)
                         (ite (and A4 A4b) 1 0)
                         (ite (and A5 A5b) 1 0)
                         (ite (and B1 B1b) 1 0)
                         (ite (and B2 B2b) 1 0)
                         (ite (and B3 B3b) 1 0)
                         (ite (and B4 B4b) 1 0)
                         (ite (and B5 B5b) 1 0)
                         (ite (and C1 C1b) 1 0)
                         (ite (and C2 C2b) 1 0)
                         (ite (and C3 C3b) 1 0)
                         (ite (and C4 C4b) 1 0)
                         (ite (and C5 C5b) 1 0)
                         (ite (and D1 D1b) 1 0)
                         (ite (and D2 D2b) 1 0)
                         (ite (and D3 D3b) 1 0)
                         (ite (and D4 D4b) 1 0)
                         (ite (and D5 D5b) 1 0)
                         (ite (and E1 E1b) 1 0)
                         (ite (and E2 E2b) 1 0)
                         (ite (and E3 E3b) 1 0)
                         (ite (and E4 E4b) 1 0)
                         (ite (and E5 E5b) 1 0)))

(define-const nanb Int (+ (ite (and A1 (not A1b)) 1 0)
                          (ite (and A2 (not A2b)) 1 0)
                          (ite (and A3 (not A3b)) 1 0)
                          (ite (and A4 (not A4b)) 1 0)
                          (ite (and A5 (not A5b)) 1 0)
                          (ite (and B1 (not B1b)) 1 0)
                          (ite (and B2 (not B2b)) 1 0)
                          (ite (and B3 (not B3b)) 1 0)
                          (ite (and B4 (not B4b)) 1 0)
                          (ite (and B5 (not B5b)) 1 0)
                          (ite (and C1 (not C1b)) 1 0)
                          (ite (and C2 (not C2b)) 1 0)
                          (ite (and C3 (not C3b)) 1 0)
                          (ite (and C4 (not C4b)) 1 0)
                          (ite (and C5 (not C5b)) 1 0)
                          (ite (and D1 (not D1b)) 1 0)
                          (ite (and D2 (not D2b)) 1 0)
                          (ite (and D3 (not D3b)) 1 0)
                          (ite (and D4 (not D4b)) 1 0)
                          (ite (and D5 (not D5b)) 1 0)
                          (ite (and E1 (not E1b)) 1 0)
                          (ite (and E2 (not E2b)) 1 0)
                          (ite (and E3 (not E3b)) 1 0)
                          (ite (and E4 (not E4b)) 1 0)
                          (ite (and E5 (not E5b)) 1 0)))

(define-const An Int (+ A1i A2i A3i A4i A5i))
(define-const Bn Int (+ B1i B2i B3i B4i B5i))
(define-const Cn Int (+ C1i C2i C3i C4i C5i))
(define-const Dn Int (+ D1i D2i D3i D4i D5i))
(define-const En Int (+ E1i E2i E3i E4i E5i))

(define-const cnt Int (+ An Bn Cn Dn En))

(assert (= A1 (not A5E1)))
(assert (= A2 (not A4)))
(assert (= A3 A3b))
(assert (= A4 (not A2)))
(assert (= A5 E5))

(assert (= B1 (not B1b)))
(assert (= B2 (and anycol anyrow anydiag)))
(assert (= B3 (>= nanb 5)))
(assert (= B4 (or _2 D_)))
(assert (= B5 false))

(assert (= C1 A1E5))
(assert (= C2 C2))
(assert (= C3 (or (not C3) C3b)))
(assert (= C4 (<= Cn 3)))
(assert (= C5 C5))

(assert (= D1 D4))
(assert (= D2 (<= cnt 17)))
(assert (= D3 (>= numcol 2)))
(assert (= D4 D1))
(assert (= D5 (>= numb 3)))

(assert (= E1 E1b))
(assert (= E2 (= (mod npb 2) 0)))
(assert (= E3 (>= (- 25 npb) 10)))
(assert (= E4 anydiag))
(assert (= E5 A5))

(check-sat)
(get-value (A1 B1 C1 D1 E1 A2 B2 C2 D2 E2 A3 B3 C3 D3 E3 A4 B4 C4 D4 E4 A5 B5 C5 D5 E5))

?