(declare-fun f (Int) Int)

(declare-fun p (Int) Bool)

(declare-fun q (Int) Bool)


(assert

(forall

((x Int))

(implies

(and (

(and (

)

)

)


(assert

(forall ((x Int) (y Int))

(implies

(and

(not (= x y))

(

(<= x 6)

(

(<= y 6)

)

(not (= (f x) (f y)))

)

)

)


(assert

(forall

((x Int))

(implies

(and (

(iff (p x) (q (f x)))

)

)

)


(assert (iff (p 1) (p 6)))


(assert

(iff

(p 2)

(and

(not (q 1))

(not (q 3))

(not (q 4))

(not (q 6))

)

)

)


(assert (iff (p 3) (not (q 2))))


(assert

(iff

(p 4)

(and

(not (p 5))

(not (p 6))

)

)

)


(assert

(iff

(p 5)

(and

(= (f 1) 6)

(= (f 2) 5)

(= (f 3) 4)

(= (f 4) 3)

(= (f 5) 2)

(= (f 6) 1)

)

)

)


(assert

(iff

(p 6)

(exists

((a Int) (b Int))

(and

(not (= a b))

(

(

(<= a 6)

(<= b 6)

(forall

((c Int))

(implies

(and (

(iff (p c) (or (= a c) (= b c)))

)

)

)

)

)

)


(check-sat)

(get-model)


과제가 너무 하기 싫어서 딴짓. 언어는 SMT-LIB 2.0.

https://rise4fun.com/Z3/tutorial/guide 에서 검사 가능.


출력된 모형의


(define-fun p!5 ((x!0 Int)) Bool

(ite (= x!0 1) true

(ite (= x!0 6) true

false)))


에서 1과 6이 참말쟁이이고 나머지가 거짓말쟁이일 경우 모든 조건을 만족함을 확인.


또한 새로운 조건


(assert

(or

(not (p 1))

(p 2)

(p 3)

(p 4)

(p 5)

(not (p 6))

)

)


를 추가한 검사 결과가 unsat 이므로 상기한 모형이 유일한 해답임을 알 수 있음.