Сложность поиска решения системы SMT с квантификатором

Question

Мне нужно найти решение проблемы путем генерации с использованием z3py. Формулы генерируются в зависимости от ввода пользователя. Во время генерации формул создаются временные переменные SMT, которые могут принимать только ограниченное количество значений, например, является целым числом, допускаются только четные значения. Для этого случая пусть временные переменные будут a и b, а их связь с глобальными переменными x и y определяется предикатом P(a,b,x,y).

Пример, сгенерированный с использованием SMT-LIB-подобного синтаксиса:

(set-info :status unknown)
(declare-fun y () Int)
(declare-fun x () Int)
(assert
(forall (
    (a Int) (b Int) (z Int) )
    (let 
      (($x22 (exists ((z Int))(and (< x z) (> z y)))))
      (=> 
          P(a, b, x, y) 
          $x22))))
(check-sat)

, где

• z - это переменная, все возможные значения которой должны быть учтены
• a и b представляют переменные, допустимые значения которых ограничены предикатом P
• переменные 'x' и 'y' должны быть вычислены, для которых выполняется формула.

Вопросы:

• Уменьшает ли предикат P время, необходимое z3 для поиска решения?
• В качестве альтернативы: при просмотре, что z3 выполняет поиск по всем возможным значениям для z и a, предикат P уменьшит размер пространства поиска?

Примечание : вопрос был обновлен после замечаний Левента Эркока.

Answer 1

Пример SMTLib, который вы привели (сгенерированный или написанный от руки), не имеет большого смысла для меня. У вас есть универсальное количественное определение по x и z, и внутри него вы снова количественно определяете z, и вся формула кажется бессмысленной. Но, возможно, это не ваша точка зрения, и это просто игрушка. Так что я просто проигнорирую это.

Как правило, «избыточные уравнения» (как вы выразились) не должны влиять на производительность. (Под избыточным я предполагаю, что вы имеете в виду вещи, которые можно извлечь из других представленных вами фактов?) Кроме того: a=z в приведенной выше формуле вовсе не является избыточным.

Это должно быть правдой, пока вы остаетесь в разрешимом подмножестве логик; что обычно означает линейный и без квантификатора.

Проблема здесь в том, что у вас есть квантификатор и, в частности, у вас есть вложенные квантификаторы. SMT-решатели плохо с ними справляются. (Поиск переполнения стека для многих вопросов, касающихся квантификаторов и z3.) Так что, если у вас есть проблемы с производительностью, лучшая стратегия состоит в том, чтобы увидеть, действительно ли они вам нужны. Просто взглянув на пример, который вы разместили, невозможно сказать, так как он не является обоснованным фактом. Итак, посмотрите, можете ли вы выразить свою собственность без квантификаторов.

Если вам нужны квантификаторы, тогда вы находитесь в зависимости от e-matcher и эвристики, и все ставки отменены. Я видел дикие характеристики производительности в этом случае. И если ваша цель - рассуждать с помощью квантификаторов, то я бы сказал, что решатели SMT просто не подходят вам, и вместо этого вы должны использовать теоремы для проверки теорем, такие как HOL / Isabelle / Coq и т. Д., Которые имеют встроенную поддержку квантификаторов. и логика высшего порядка.

Если вы опубликуете фактический пример того, что вы пытаетесь сделать, чтобы z3 доказал для вас, мы могли бы увидеть, есть ли другой способ сформулировать его, который мог бы упростить обработку для z3. Без конкретной цели и примера невозможно более детально оценить производительность.