Таймаут z3 для нелинейных ограничений

Question

У меня проблема с тайм-аутом при использовании z3 для нелинейной вещественной арифметики. Следующий код должен проверить, имеет ли 4-мерный гипер-прямоугольник объем больше 50000, а также удовлетворяет некоторым ограничениям. Но z3 не может дать ответ в течение 1 минуты. Как сделать это быстрее?

a0min = Real('a0min')
a0max = Real('a0max')
a1min = Real('a1min')
a1max = Real('a1max')
a2min = Real('a2min')
a2max = Real('a2max')
a3min = Real('a3min')
a3max = Real('a3max')
volume = Real('volume')

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

s.add(-a0min * (1.0 - a1max) + a2max * a3max <= -95000.0,
a0min >  0.0,
a0min < a0max,
a0max < 1000000.0,
a1min > 0.0,
a1min < a1max,
a1max < 1.0,
a2min > 1.0,
a2min < a2max,
a2max < 1000.0,
a3min > 1.0,
a3min < a3max,
a3max < 50.0,
(a0max - a0min) * (a1max -  a1min) * (a2max -  a2min) * (a3max - a3min) > 50000.0,
volume == (a0max - a0min) * (a1max -  a1min) * (a2max -  a2min) * (a3max - a3min))
print s.check()

И есть интересная вещь: если заменить некоторые из ">" и "<" на "<=" и ">=", решатель z3 может вернуть ответ через две секунды. Соответствующий код выглядит следующим образом. Кто-нибудь знает, почему это происходит?

a0min = Real('a0min')
a0max = Real('a0max')
a1min = Real('a1min')
a1max = Real('a1max')
a2min = Real('a2min')
a2max = Real('a2max')
a3min = Real('a3min')
a3max = Real('a3max')
volume = Real('volume')

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

s.add(-a0min * (1.0 - a1max) + a2max * a3max <= -95000.0,
a0min >=  0.0,
a0min <= a0max,
a0max <= 1000000.0,
a1min >= 0.0,
a1min <= a1max,
a1max <= 1.0,
a2min >= 1.0,
a2min <= a2max,
a2max <= 1000.0,
a3min >= 1.0,
a3min <= a3max,
a3max <= 50.0,

(a0max - a0min) * (a1max -  a1min) * (a2max -  a2min) * (a3max - a3min) > 50000.0,
volume == (a0max - a0min) * (a1max -  a1min) * (a2max -  a2min) * (a3max - a3min))
print s.check()

Answer 1

В первом случае Z3 "завис", вычисляя с действительными алгебраическими числами. Если мы выполним ваш скрипт с

 valgrind --tool=callgrind python nl.py

Прервите через несколько минут и бегите

 kcachegrind 

Мы увидим, что Z3 застрял внутри algebraic_numbers::isolate_roots, Текущий пакет действительных алгебраических чисел, используемый nlsat решатель очень неэффективен. У нас есть новый пакет для вычислений с алгебраическими числами, но он не интегрирован с nlsat еще.

Одним из способов избежать вычислений алгебраических чисел является использование только строгих неравенств. Равенство volume == ... безвреден, поскольку устраняется во время предварительной обработки. Если мы заменим первое ограничение на -a0min * (1.0 - a1max) + a2max * a3max < -95000.0, затем Z3 также быстро завершается (также доступно онлайн здесь).

a0min = Real('a0min')
a0max = Real('a0max')
a1min = Real('a1min')
a1max = Real('a1max')
a2min = Real('a2min')
a2max = Real('a2max')
a3min = Real('a3min')
a3max = Real('a3max')
volume = Real('volume')

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

s.add(-a0min * (1.0 - a1max) + a2max * a3max < -95000.0,
a0min >  0.0,
a0min < a0max,
a0max < 1000000.0,
a1min > 0.0,
a1min < a1max,
a1max < 1.0,
a2min > 1.0,
a2min < a2max,
a2max < 1000.0,
a3min > 1.0,
a3min < a3max,
a3max < 50.0,
(a0max - a0min) * (a1max -  a1min) * (a2max -  a2min) * (a3max - a3min) > 50000.0,
volume == (a0max - a0min) * (a1max -  a1min) * (a2max -  a2min) * (a3max - a3min))
print s.check()
print s.model()

Кстати, когда вы заменяете все на <=, nlsat все еще должен использовать реальные алгебраические вычисления, но изменение влияет на nlsat дерево поиска, и ему удается найти решение, прежде чем оно застрянет в вычислении реального алгебраического числа.

Вот три места, где nlsat застревает в примерах, которые мы пробовали / исследовали

• Вычисления действительных алгебраических чисел (как ваш пример). Это будет исправлено, когда мы заменим текущий пакет новым.

• Полиномиальная факторизация. Текущий алгоритм, реализованный в Z3, очень неэффективен. Это также можно исправить.

• Субрезультатные вычисления. Это сложно, поскольку, насколько я знаю, Z3 использует очень эффективную реализацию. Производительность аналогична реализации в современных системах, таких как Mathematica. Эта операция используется, когда Z3 выполняет поиск в обратном направлении. Приятным свойством является то, что мы можем доказать, что Z3 всегда будет завершаться с использованием этого подхода. Одна альтернатива состоит в том, чтобы рассмотреть приблизительные методы, которые не гарантируют завершение, но являются более дешевыми. К сожалению, это не незначительное изменение, как два предыдущих.