Ликвидация квантификатора - Дополнительные вопросы

Question

Большое спасибо Джошу и Леонардо за ответ на предыдущий вопрос.

У меня есть еще несколько вопросов.

<1> Рассмотрим другой пример.

(exists k) i * k > = 4 and k > 1.

Это имеет простое решение i > 0. (как для Int, так и для Real)

Тем не менее, когда я попытался следовать,

(declare-const i Int)
(assert (exists ((k Int)) (and (>= (* i k)  4) (> k 1))))
(apply (using-params qe :qe-nonlinear true))

Z3 Не удалось устранить квантификатор здесь.

Тем не менее, это может устранить для реального случая. (когда i и k оба являются действительными числами) Является ли устранение квантификатора сложнее для целых чисел?

<2> Я использую Z3 C API в моей системе. Я добавляю некоторые нелинейные ограничения на целые числа с квантификаторами в моей системе. Z3 в настоящее время проверяет на удовлетворенность и дает мне правильную модель, когда система является удовлетворительной.

Я знаю, что после исключения кванторов эти ограничения сводятся к линейным ограничениям.

Я думал, что z3 делает устранение квантора автоматически перед проверкой выполнимости. Но так как он не мог сделать это в случае 1 выше, я теперь думаю, что он обычно находит модель без исключения Quantifier. Я прав?

В настоящее время z3 может решить ограничения в моей системе. Но это может дать сбой в сложных системах. В таком случае, будет ли хорошей идеей сделать удаление кванторов каким-либо другим методом без z3 и добавить ограничения к z3 позже?

<3> Я могу подумать о добавлении вещественных нелинейных ограничений вместо целочисленных нелинейных ограничений в моей системе. В таком случае, как я могу заставить z3 выполнять удаление квантификаторов с помощью C-API?

<4> И, наконец, является ли хорошей идеей заставить z3 выполнять удаление квантификаторов? Или он обычно находит модель более разумно, не выполняя Quantifier Elission?

Благодарю.

Answer 1

<1> Теория нелинейной целочисленной арифметики не допускает исключения кванторов (qe). Более того, задача решения для нелинейной целочисленной арифметики неразрешима.

Напомним, что Z3 имеет ограниченную поддержку для устранения кванторов нелинейных вещественных арифметических формул. Текущая процедура основана на замене виртуального термина. Будущие версии, возможно, будут иметь полную поддержку нелинейной вещественной арифметики.

<2> Исключение квантификатора не включено по умолчанию. Пользователь должен запросить это. Z3 может найти модели для удовлетворительных формул, даже если исключение квантификатора не включено. Он использует технику, называемую основанной на модели квантификатором (MBQI). Онлайновое руководство по Z3 содержит несколько примеров, описывающих возможности и ограничения этой техники.

<3> Вы должны включить его при создании объекта Z3_context. Любая опция, заданная в командной строке, может быть предоставлена ​​при создании объекта Z3_context. Вот пример, который позволяет построить модель и исключить квантификатор:

Z3_config cfg = Z3_mk_config();
Z3_context ctx;
Z3_set_param_value(cfg, "MODEL", "true");
Z3_set_param_value(cfg, "ELIM_QUANTIFIERS", "true");
Z3_set_param_value(cfg, "ELIM_NLARITH_QUANTIFIERS", "true");
ctx = mk_context_custom(cfg, throw_z3_error);
Z3_del_config(cfg);

После этого, ctx указывает на объект контекста Z3, который поддерживает построение модели и устранение квантификатора.

<4> Модуль MBQI не является полным даже для линейного арифметического фрагмента. Онлайновое руководство по Z3 описывает фрагменты, которые оно завершает. Модуль MBQI является хорошим вариантом для задач, которые содержат неинтерпретированные функции. Если в ваших задачах используется только арифметика, то устранение квантификаторов обычно лучше и эффективнее. При этом, несколько проблем могут быть быстро решены с помощью MBQI.