old vs new version of Z3

Question

У меня есть экземпляр, который можно было бы очень эффективно решить старой версией Z3 (версия 2.18). Он возвращает SAT через несколько секунд. Однако, когда я пытаюсь использовать текущую версию Z3 (версия 4.3.1). Он не возвращает результат через 10 минут.

Вот некоторые подробности об эксперименте. Может ли кто-нибудь дать совет?

• есть 4000 Bool переменные и 200 Int переменных

• все ограничения находятся в логике высказываний со сравнением между целыми числами, как < б

• платформы: открытым SUSE Linux 12.3@thinkpad T400s

• Z3 v2.18 был загружен как linux binary в прошлом году (я не могу найти ссылку сейчас)

• Z3 v4.3.1 был загружен в виде исходного кода, и я скомпилировать его на моем ноутбуке с помощью настройки

Есть около 50000 строк в файле по умолчанию пгт, поэтому я не могу разместить его здесь. Я был бы рад отправить файл по электронной почте, если кто-нибудь заинтересован. Спасибо.

Answer 1

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

Примечание: автор отправил свой бенчмарк по электронной почте авторам Z3.

В филиале «работа в прогресс», мне удалось воспроизвести работу Z3 2.19 с помощью

  (set-option :smt.auto-config false) 

Here инструкции о том, как загрузить ветку «работа-в-Прогресс».

Чтобы получить такое же поведение, мы также должны заменить (чек-сат) с (чек-СБ-с помощью ЗПТ)

Кстати, в официальном релизе, мы должны использовать

  (set-option :auto-config false) 

вместо

  (set-option :smt.auto-config false)