У меня есть огромный набор линейных вещественных арифметических ограничений, которые нужно решить, и я постепенно передаю их решателю. Z3 всегда, кажется, застревает через некоторое время. Собирается ли Z3 изменить свою стратегию при разрешении ограничений, например, отказаться от симплексного алгоритма и попробовать другие и т. д. Или я должен явно проинструктировать Z3 сделать это? Я использую Z3py.
Будет ли Z3 адаптивно менять стратегию решения линейных вещественных арифметических ограничений?
comment
Похоже, вы относительно новичок в Stack Overflow, или, по крайней мере, вы не очень много публиковали. Вы получите лучший ответ здесь, если вы (1) сделаете свои вопросы более конкретными и предоставите явные примеры и (2) примете ответы хотя бы на некоторые из ваших вопросов.
- person Douglas B. Staple schedule 29.07.2016
Ответы (1)
Без дополнительных подробностей невозможно точно ответить на этот вопрос.
Как правило, без установки логики и запуска тактики по умолчанию или вызова (check-sat) без дополнительных параметров, Z3 переключится на другой решатель в первый раз, когда увидит команду push; до этого он может использовать неинкрементный решатель.
Инкрементальный решатель имеет все положительные и отрицательные стороны инкрементных решателей, т. е. он может быть быстрее изначально, но через некоторое время он может не использовать ранее изученные леммы, и он может просто помнить слишком много нерелевантных фактов. Кроме того, эвристика может «запоминать» информацию, которая не применяется в более позднее время, например, «хороший» порядок переменных может измениться на плохой после того, как все будет извлечено, и будет запущена другая проблема с теми же переменными. В прошлом некоторые пользователи обнаружили, что для них лучше использовать инкрементный решатель для некоторого количества запросов, но начинать с нуля, когда он становится слишком медленным.
person
Christoph Wintersteiger
schedule
21.07.2016
