Экземпляр QF_AUFBV имеет одно невероятно сложное предположение

Код smt2, сброшенный из Z3py, находится здесь. Если вы прокрутите вниз, вы увидите, что есть одно предположение, которое, если его прокомментировать, сразу же решает проблему.

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

  • Правильно ли я выбрал теорию, QF_AUFBV?
  • Почему предположение делает этот пример намного сложнее?
  • Есть какие-нибудь подсказки, как его отлаживать?

Я решил подобные случаи, и они довольно быстрые.

Когда я решаю это из Z3py с verbose = 10, я вижу такой результат, пока он решает:

(smt.restarting :propagations 35577 :decisions 13935 :conflicts 277 :restart 110 :restart-outer 110 :agility 0.0356467)
(smt.restarting :propagations 40109 :decisions 15040 :conflicts 388 :restart 100 :restart-outer 121 :agility 0.0452989)
(smt.restarting :propagations 43945 :decisions 15901 :conflicts 489 :restart 110 :restart-outer 121 :agility 0.0671191)

Не уверен, что это полезно. Спасибо.


z3 z3py
person EfForEffort    schedule 07.05.2015    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Небольшие изменения во входных данных часто имеют огромное влияние на время выполнения Z3s, особенно если они дизъюнктивны (как ваше предположение). Похоже, что в этой проблеме решатель ядра SMT просто застревает в поисках решения и, попробовав тысячи ветвей (:decisions 13935), решает сдаться и начать с нуля (smt.restarting...).

Выбор теории в порядке. Если вам не нужны UF, вы можете установить его на QF_ABV, но по умолчанию Z3 будет использовать для них ту же тактику / параметры.

Я не уверен, что вижу, где есть ошибка для «отладки», но я полагаю, что под «отладкой» вы имеете в виду «ускорить работу»?

person Christoph Wintersteiger    schedule 08.05.2015
comment
Я знаю, что время решения варьируется (иногда сильно) от решателя к решателю, но Boolector может мгновенно решить этот пример. Думаю, мне было интересно, есть ли какие-то подходящие тактики, которые я мог бы попробовать, или альтернативная кодировка, или некоторые параметры решателя, о которых я мог бы установить, о которых я не знал. Спасибо, что посмотрели. - person EfForEffort; 10.05.2015