У меня есть экземпляр, который может быть очень эффективно решен старой версией Z3 (версия 2.18). Он возвращает SAT через несколько секунд. Однако когда я пробую его на текущей версии Z3 (версия 4.3.1). По прошествии 10 минут не возвращает никакого результата.
Вот некоторые подробности эксперимента. Может ли кто-нибудь дать совет?
есть 4000 переменных типа Bool и 200 переменных типа Int.
все ограничения находятся в логике высказываний со сравнением между целыми числами, такими как a ‹b
платформа: open suse linux 12.3@thinkpad T400s
Z3 v2.18 был загружен как двоичный файл linux в прошлом году (сейчас я не могу найти ссылку)
Z3 v4.3.1 был загружен как исходный код, и я компилирую его на своем ноутбуке, используя настройки по умолчанию
В smt файле около 50 000 строк, поэтому я не могу его сюда выложить. Если кому-то интересно, я с удовольствием отправлю файл по электронной почте. Спасибо.
