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