Кодирование возвращает неизвестно

В вашем сценарии используется тактика

s = Then('simplify','smt').solver()

Эта тактика применяет упрощение Z3, а затем выполняет решатель SMT «общего назначения», доступный в Z3. Этот решатель не подходит для нелинейной арифметики. Он основан на комбинации: симплексной, интервальной арифметики и базиса Гробнера. Одним из больших ограничений этого модуля является то, что он не может найти модели/решения, содержащие иррациональные числа. В будущем мы заменим этот модуль новыми нелинейными решателями, доступными в Z3.

Для нелинейной арифметики мы обычно предлагаем решатель nlsat, доступный в Z3. Это полная процедура, и обычно она очень эффективна для неудовлетворительных и удовлетворительных случаев. Подробнее о nlsat можно узнать в этой статье. Чтобы использовать nlsat, мы должны использовать

s = Tactic('qfnra-nlsat').solver()

К сожалению, в вашем примере nlsat застрянет. Он застрянет при вычислении подрезультатов очень больших полиномов, полученных во время решения.

Z3 имеет еще один движок для обработки нелинейной арифметики. Этот движок сводит проблему к SAT. Он эффективен только для разрешимых задач, решения которых имеют вид a + b sqrt(2), где a и b — рациональные числа. Используя этот движок, мы можем решить вашу проблему за очень короткое время. Прикрепил результат в конце поста. Чтобы использовать этот движок, мы должны использовать

s = Then('simplify', 'nla2bv', 'smt').solver()

EDIT Более того, тактика nla2bv кодирует рациональные числа a и b как пару битовых векторов. По умолчанию используются битовые векторы размера 4. Однако это значение можно указать с помощью опции nlsat_bv_size. Это не глобальная опция, а опция, предоставляемая тактике nla2bv. Таким образом, nla2bv может найти решения только в форме a + b sqrt(2), где a и b можно закодировать, используя небольшое количество битов. Если разрешимая задача не имеет решения в такой форме, эта тактика потерпит неудачу и вернет unknown. ЗАВЕРШИТЬ РЕДАКТИРОВАНИЕ

Ваш пример также предполагает, что мы должны улучшить nlsat и сделать его более эффективным в качестве процедуры поиска модели/решения. Текущая версия зависает при попытке показать, что проблема не имеет решения. Мы знаем об этих ограничениях и работаем над новыми процедурами их обхода.

Кстати, в интерфейсе Python Z3 отображает модели/решения в десятичной системе счисления. Однако все просчитано точно. Чтобы получить точное представление решения. Мы можем использовать метод sexpr(). Например, я изменил ваш цикл на

for d in m.decls():
    print "%s = %s = %s" % (d.name(), m[d], m[d].sexpr())

В новом цикле я показываю результат в десятичном представлении и внутреннем точном. Смысл (root-obj (+ (* 2 (^ x 2)) (* 12 x) (- 7)) 2) - корень 2-го многочлена 2*x^2 + 12x - 7.

РЕДАКТИРОВАНИЕ Z3 предоставляет комбинаторы для создания нетривиальных решателей. В приведенных выше примерах мы использовали Then для выполнения последовательной композиции различных тактик. Мы также можем использовать OrElse, чтобы попробовать другую тактику. и TryFor(t, ms), который пытается использовать тактику t в течение ms миллисекунд и терпит неудачу, если проблема не может быть решена за заданное время. Эти комбинаторы можно использовать для создания тактик, использующих различные стратегии для решения проблемы. ЗАВЕРШИТЬ РЕДАКТИРОВАНИЕ

sat
Presenting results
traversing model...
s_2_p_p = 0.5355339059? = (root-obj (+ (* 2 (^ x 2)) (* 12 x) (- 7)) 2)
s_1_p_p = 0 = 0.0
s_init_p_p = 0.2928932188? = (root-obj (+ (* 2 (^ x 2)) (* (- 4) x) 1) 1)
s_2_p = 0.7071067811? = (root-obj (+ (* 2 (^ x 2)) (- 1)) 2)
s_1_p = 0 = 0.0
s_init_p = 0.2928932188? = (root-obj (+ (* 2 (^ x 2)) (* (- 4) x) 1) 1)
epsilon = 0 = 0.0
p_b2_s2_s_sink = 0.9142135623? = (root-obj (+ (* 4 (^ x 2)) (* 4 x) (- 7)) 2)
p_b2_s2_s_target = 0.0857864376? = (root-obj (+ (* 4 (^ x 2)) (* (- 12) x) 1) 1)
p_b2_s2_s_2 = 0 = 0.0
p_b2_s2_s_1 = 0 = 0.0
p_a2_s2_s_sink = 0 = 0.0
p_a2_s2_s_target = 0.8284271247? = (root-obj (+ (^ x 2) (* 4 x) (- 4)) 2)
p_a2_s2_s_2 = 0.1715728752? = (root-obj (+ (^ x 2) (* (- 6) x) 1) 1)
p_a2_s2_s_1 = 0 = 0.0
sigma_s2_b2 = 1 = 1.0
sigma_s2_a2 = 0 = 0.0
p_b1_s1_s_sink = 1 = 1.0
p_b1_s1_s_target = 0 = 0.0
p_b1_s1_s_2 = 0 = 0.0
p_b1_s1_s_1 = 0 = 0.0
p_a1_s1_s_sink = 1 = 1.0
p_a1_s1_s_target = 0 = 0.0
p_a1_s1_s_2 = 0 = 0.0
p_a1_s1_s_1 = 0 = 0.0
sigma_s1_b1 = 0 = 0.0
sigma_s1_a1 = 1 = 1.0
p_sinit_sink = 0.7071067811? = (root-obj (+ (* 2 (^ x 2)) (- 1)) 2)
p_sinit_target = 0.2928932188? = (root-obj (+ (* 2 (^ x 2)) (* (- 4) x) 1) 1)
p_sinit_2 = 0 = 0.0
p_sinit_1 = 0 = 0.0
s_sink = 0 = 0.0
s_target = 1 = 1.0
s_2 = 0.0857864376? = (root-obj (+ (* 4 (^ x 2)) (* (- 12) x) 1) 1)
s_1 = 0 = 0.0
s_init = 0.2928932188? = (root-obj (+ (* 2 (^ x 2)) (* (- 4) x) 1) 1)

EDIT Вы можете решить проблему в своем комментарии, используя тактику

s = Then('simplify', 'nlsat').solver()

Эта тактика решит проблему за пару секунд и выдаст решение в конце поста. Как я уже говорил выше, nlsat завершен, но это может занять очень много времени. Ваша проблема находится на грани того, что текущая версия Z3 может решать/решать автоматически. Мы можем комбинировать различные тактики с OrElse и TryFor, чтобы сделать его более стабильным. Пример:

s = OrElse(TryFor(Then('simplify', 'nla2bv', 'smt', 'fail-if-undecided'), 1000),
           TryFor(Then('simplify', 'nlsat'), 1000),
           TryFor(Then('simplify', 'nla2bv', 'smt', 'fail-if-undecided'), 10000),
           Then('simplify', 'nlsat')).solver()

Приведенная выше тактика пробует подход nla2bv в течение 1 секунды, затем nlsat в течение 1 секунды, затем nla2bv в течение 10 секунд и, наконец, nlsat без тайм-аута.

Я знаю, что это не идеальное решение, но подобные вариации могут быть полезными обходными путями, пока не будет готов следующий решатель для нелинейной арифметики. Более того, в Z3 есть много других тактик, которые можно использовать для упрощения/предварительной обработки проблемы до того, как мы вызовем nlsat. ЗАВЕРШИТЬ РЕДАКТИРОВАНИЕ

s_init = 15/32
s_1 = 7/16
s_2 = 1/2
s_target = 1
s_sink = 0
p_sinit_1 = 1/2
p_sinit_2 = 1/4
p_sinit_target = 1/8
p_sinit_sink = 1/8
sigma_s1_a1 = 1/2
sigma_s1_b1 = 1/2
p_a1_s1_s_1 = 1/2
p_a1_s1_s_2 = 1/4
p_a1_s1_s_target = 1/8
p_a1_s1_s_sink = 1/8
p_b1_s1_s_1 = 1/2
p_b1_s1_s_2 = 1/4
p_b1_s1_s_target = 1/16
p_b1_s1_s_sink = 3/16
sigma_s2_a2 = 1/2
sigma_s2_b2 = 1/2
p_a2_s2_s_1 = 1/2
p_a2_s2_s_2 = 1/4
p_a2_s2_s_target = 11/64
p_a2_s2_s_sink = 5/64
p_b2_s2_s_1 = 3/4
p_b2_s2_s_2 = 1/32
p_b2_s2_s_target = 9/64
p_b2_s2_s_sink = 5/64
epsilon = 1/4
s_init_p = 1649/3520
s_1_p = 797/1760
s_2_p = 103/220
s_init_p_p = 1809/3904
s_1_p_p = 813/1952
s_2_p_p = 127/244

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

• Мы можем включить подробные сообщения с помощью команды: set_option("verbose", 10). Число — это уровень детализации: 0 == «нет сообщений», а более высокие числа == «больше сообщений».

• Скомпилируйте Z3 с поддержкой трассировки. Дополнительную информацию см. в этом сообщении.

• Создайте журнал API-интерфейсов Z3, вызванных программой Python, с помощью команды open_log("z3.log"). Эту команду следует вызывать перед любым другим вызовом Z3 API. Затем запустите журнал, используя исполняемый файл z3 внутри gdb. Таким образом, вы сможете остановить выполнение и найти, где застрял Z3. Решатель nlsat обычно застревает в двух разных местах:

  1. Вычисление промежуточных результатов (процедура psc_chain будет в стеке), и

  2. выделение корней многочленов с алгебраическими коэффициентами (процедура isolate_roots будет на стеке).

Проблема 2 будет скоро решена после того, как мы заменим старый пакет алгебраических чисел на новый, который намного эффективнее. К сожалению, кажется, что ваши проблемы застряли на промежуточном этапе.

Еще одно замечание: хотя nla2bv было эффективным для вашего исходного теста, маловероятно, что ваши новые тесты будут иметь решение в форме a + b sqrt(2), где a и b — рациональные числа. Таким образом, использование nla2bv просто накладно. Тактика nlsat предполагает, что проблема в CNF. Итак, для pastebin.com/QRCUQE10 мы должны вызвать tseitin-cnf перед вызовом nlsat. Другой вариант — использовать «большую» тактику qfnra-nlsat. Он вызывает множество шагов предварительной обработки перед вызовом nlsat. Однако некоторые из этих шагов могут затруднить решение некоторых проблем.

ЗАВЕРШИТЬ ИЗМЕНЕНИЕ 2