Патрик: Возможно, можно использовать предикаты «переполнения / недополнения» Z3 (как расширение SMTLib) для определения состояния и получения результатов через битовые векторы. Но, по моему опыту, если у вас уже нет хорошей идеи, где находится решение, оно быстро превращается в бесконечное добавление ограничений, запрещающих ложные модели. Я хотел бы знать, был ли вообще применимый прием, хотя я сомневаюсь, что он существует.

возможно, я хотел бы получить второе мнение о моем коде.

Ограничения проблемы:

a,b,c,d,e,f ненулевые целые числаs1 = [a,b,c] а такжеs2 = [d,e,f] наборыСуммаs1_i + s2_j заi,j = 0..2 должен быть идеальным квадратом

Я не понимаю, почему, но мой код возвращает модель не доступна. Более того, при комментировании следующие строки:

(assert (and (> sqrtx4 1) (= x4 (* sqrtx4 sqrtx4))))
(assert (and (> sqrtx5 1) (= x5 (* sqrtx5 sqrtx5))))
(assert (and (> sqrtx6 1) (= x6 (* sqrtx6 sqrtx6))))

(assert (and (> sqrtx7 1) (= x7 (* sqrtx7 sqrtx7))))
(assert (and (> sqrtx8 1) (= x8 (* sqrtx8 sqrtx8))))
(assert (and (> sqrtx9 1) (= x9 (* sqrtx9 sqrtx9))))

Значения d, e, f отрицательны. Нет никаких ограничений, которые требуют от них этого. Мне интересно, возможно, есть какие-то скрытые ограничения, которые проникли внутрь и испортили модель.

Действительное ожидаемое решение будет:

a = 3
b = 168
c = 483
d = 1
e = 193
f = 673

редактировать: вставка(assert (= a 3)) а также(assert (= b 168)) в результате решатель находит правильные значения. Это только озадачивает меня дальше.

Полный код:

(declare-fun sqrtx1 () Int)
(declare-fun sqrtx2 () Int)
(declare-fun sqrtx3 () Int)
(declare-fun sqrtx4 () Int)
(declare-fun sqrtx5 () Int)
(declare-fun sqrtx6 () Int)
(declare-fun sqrtx7 () Int)
(declare-fun sqrtx8 () Int)
(declare-fun sqrtx9 () Int)

(declare-fun a     () Int)
(declare-fun b     () Int)
(declare-fun c     () Int)
(declare-fun d     () Int)
(declare-fun e     () Int)
(declare-fun f     () Int)

(declare-fun x1     () Int)
(declare-fun x2     () Int)
(declare-fun x3     () Int)
(declare-fun x4     () Int)
(declare-fun x5     () Int)
(declare-fun x6     () Int)
(declare-fun x7     () Int)
(declare-fun x8     () Int)
(declare-fun x9     () Int)


;all numbers are non-zero integers
(assert (not (= a 0)))
(assert (not (= b 0)))
(assert (not (= c 0)))
(assert (not (= d 0)))
(assert (not (= e 0)))
(assert (not (= f 0)))

;both arrays need to be sets
(assert (not (= a b)))
(assert (not (= a c)))
(assert (not (= b c)))

(assert (not (= d e)))
(assert (not (= d f)))
(assert (not (= e f)))



(assert (and (> sqrtx1 1) (= x1 (* sqrtx1 sqrtx1))))
(assert (and (> sqrtx2 1) (= x2 (* sqrtx2 sqrtx2))))
(assert (and (> sqrtx3 1) (= x3 (* sqrtx3 sqrtx3))))


(assert (and (> sqrtx4 1) (= x4 (* sqrtx4 sqrtx4))))
(assert (and (> sqrtx5 1) (= x5 (* sqrtx5 sqrtx5))))
(assert (and (> sqrtx6 1) (= x6 (* sqrtx6 sqrtx6))))

(assert (and (> sqrtx7 1) (= x7 (* sqrtx7 sqrtx7))))
(assert (and (> sqrtx8 1) (= x8 (* sqrtx8 sqrtx8))))
(assert (and (> sqrtx9 1) (= x9 (* sqrtx9 sqrtx9))))

;all combinations of sums need to be squared
(assert (= (+ a d) x1))
(assert (= (+ a e) x2))
(assert (= (+ a f) x3)) 

(assert (= (+ b d) x4))
(assert (= (+ b e) x5))
(assert (= (+ b f) x6))

(assert (= (+ c d) x7))
(assert (= (+ c e) x8))
(assert (= (+ c f) x9))


(check-sat-using (then simplify solve-eqs smt))
(get-model)
(get-value (a))
(get-value (b))
(get-value (c))
(get-value (d))
(get-value (e))
(get-value (f))

Ответы на вопрос(1)

Ваш ответ на вопрос