Z3 возвращает модель недоступна

Question

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

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

• 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))

Answer 1

Нелинейная целочисленная арифметика неразрешима.Это означает, что не существует процедуры принятия решения, которая могла бы решить, что произвольные нелинейные целочисленные ограничения могут быть выполнены.Это то, что z3 говорит вам, когда в ответе на ваш запрос говорит «неизвестно».

Это, конечно, не означает, что на отдельные случаи невозможно ответить.У Z3 есть определенная тактика, которую он применяет для решения таких формул, но он по сути ограничен в том, что он может обрабатывать.Ваша проблема относится к той категории: та, которую Z3 просто не в состоянии решить.

Z3 имеет специальную тактику NRA (нелинейная вещественная арифметика), которую вы можете использовать.Он по существу рассматривает все переменные как вещественные, решает проблему (нелинейная вещественная арифметика разрешима, и z3 может найти все алгебраические вещественные решения), а затем проверяет, являются ли результаты на самом деле целочисленными.Если нет, он пытается другое решение по реалам.Иногда эта тактика может обрабатывать нелинейные целочисленные задачи, если вам удастся найти правильное решение.Вы можете запустить его, используя:

(check-sat-using qfnra)

К сожалению, это не решит вашу конкретную проблему в то время, когда я позволил ему работать.(Более 10 минут.) Маловероятно, что он когда-нибудь найдет правильное решение.

У вас действительно не так много вариантов.Решатели SMT просто не подходят для нелинейных целочисленных задач.Фактически, как я упоминал выше, не существует инструмента, который мог бы обрабатывать произвольные нелинейные целочисленные задачи из-за неразрешимости;но некоторые инструменты работают лучше, чем другие, в зависимости от алгоритмов, которые они используют.

Когда вы говорите z3, что такое a и b, вы по существу отбираете большую часть нелинейности, а остальное становитсяпросты в обращении.Вполне возможно, что вы сможете найти последовательность применяемых тактик, которая решит ваш оригинал, но такие приемы очень хрупки на практике и их нелегко обнаружить;поскольку вы по сути вводите эвристику в поиск, и у вас нет большого контроля над тем, как она себя ведет.

Примечание: ваш скрипт может быть немного улучшен.Чтобы выразить, что все числа разные, используйте отдельный предикат:

(assert (distinct (a b c)))
(assert (distinct (d e f)))