Квантификатор против неквантификатора

У меня вопрос по квантификаторам.

Предположим, что у меня есть массив, и я хочу вычислить индекс массива 0, 1 и 2 для этого массива -

(declare-const cpuA (Array Int Int))
(assert (or (= (select cpuA 0) 0) (= (select cpuA 0) 1))) 
(assert (or (= (select cpuA 1) 0) (= (select cpuA 1) 1))) 
(assert (or (= (select cpuA 2) 0) (= (select cpuA 2) 1)))

Или иначе я могу указать то же самое, используя конструкцию forall, как -

(assert (forall ((x Int)) (=> (and (>= x 0) (<= x 2)) (or (= (select cpuA x) 0) (= (select cpuA x) 1)))))

Теперь я хотел бы понять разницу между двумя из них. Первый метод выполняется быстро и дает простую и удобочитаемую модель. В отличие от второго варианта размер кода намного меньше, но для выполнения программы требуется время. И решение тоже сложное.

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


z3
person Raj    schedule 04.04.2012    source источник

Ответы (1)


arrow_upward
4
arrow_downward

Кванторные рассуждения обычно очень дороги. В вашем примере количественная формула эквивалентна трем предоставленным вами утверждениям. Однако это не то, как Z3 решает/решает вашу формулу. Z3 решает вашу формулу, используя метод, называемый созданием квантификаторов на основе моделей (MBQI). Этот метод может решить многие проблемы (см. http://rise4fun.com/Z3/tutorial/guide). ). Это в основном эффективно на фрагментах, описанных в этом руководстве. Он поддерживает неинтерпретируемые функции, арифметику и теории битовых векторов. Он также имеет ограниченную поддержку массивов и типов данных. Этого достаточно для решения вашего примера. Модель производства Z3 кажется более сложной, поскольку для решения более сложных фрагментов используется тот же движок. Модель должна выглядеть как небольшая функциональная программа. Дополнительную информацию о том, как работает этот подход, можно найти в следующих статьях:

Обратите внимание, что теория массивов в основном полезна для представления/моделирования неограниченных или больших массивов. То есть фактический размер массива неизвестен или слишком велик. Под большим я подразумеваю, что количество обращений к массиву (т. е. selects) в вашей формуле намного меньше фактического размера массива. Мы должны спросить себя: «Действительно ли нам нужны массивы для моделирования/решения проблемы X?». Вы можете рассмотреть следующие альтернативы:

  • #P5# <блочная цитата> #P6# #P7#

  • Программный API. Мы видели много примеров, когда массивы (и функции) использовались для обеспечения компактного кодирования. Компактное и элегантное кодирование не обязательно легче решить. На самом деле обычно бывает наоборот. Вы можете получить лучшее из обоих миров (производительность и компактность), используя программный API для Z3. В следующей ссылке я закодировал ваш пример, используя одну «переменную» для каждой позиции «массива». Макросы/функции используются для кодирования ограничений, таких как: выражение является 0 или 1. http://rise4fun.com/Z3Py/JF

person Leonardo de Moura    schedule 05.04.2012
comment
Дорогой Леонардо, я снова возвращаюсь к тому же вопросу. Я пытаюсь оптимизировать код для спутникового решателя. Не могли бы вы сказать мне, когда хорошо использовать константы и когда хорошо использовать неинтерпретируемые функции. Например, у меня в коде около 30-40 неинтерпретируемых функций. Когда я заменяю некоторые функции несколькими константами, например (xA 0), замененными на xA0 и т. д., я получаю сокращение времени выполнения, но для других я не получаю. Каково ключевое правило выбора между ними? Зависит ли это от того, как часто вы используете их в коде? - person Raj; 31.05.2012
comment
Колебания производительности очень распространены. Мы наблюдаем флуктуации даже тогда, когда вносим небольшие изменения, такие как переупорядочивание утверждений. Любая незначительная модификация может изменить порядок прохождения Z3 пространства поиска. Как правило, мы должны избегать квантификаторов, когда это возможно. Если мы можем закодировать проблему, используя одну теорию, мы обычно получаем лучшую производительность. Конечно, у нас всегда есть исключения. Какие колебания производительности вы наблюдаете? Это порядка 2х, 10х, 100х? - person Leonardo de Moura; 31.05.2012