Устранение Квалификатора - Дополнительные вопросы

Question

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

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

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

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

Это простое решение я> 0. (как для Int и реальный случай)

Однако, когда я попытался следующие,

(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> Я использую API Z3 C в своей системе. Я добавляю некоторые нелинейные ограничения на целые числа с кванторами в моей системе. Z3 в настоящее время проверяет работоспособность и дает мне правильную модель, когда система является выполнимой.

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

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

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

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

< 4> Наконец, это хорошая идея, чтобы обеспечить соблюдение Z3 для устранения Квантификатора? Или он обычно находит модель более разумно, не делая Устранение Квантера?

Спасибо.

Answer 1

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

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

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

< 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.