выполнение нескольких вызовов (check-sat) до тех пор, пока он не вернет unsat

В примечаниях к выпуску z3 версии 4.6 упоминается новая функция «выполнение нескольких вызовов (check-sat) до тех пор, пока он не вернет unsat». Является ли это эквивалентом для ALLSAT?
Где я могу найти дополнительную документацию или пример для этой функции?


z3
person ChristianJ    schedule 05.02.2018    source источник
comment
Да, это про вызовы Оптимизации. Это не связано с AllSAT. Для ALL-SAT нет встроенного метода.   -  person Nikolaj Bjorner    schedule 06.02.2018

Ответы (1)


arrow_upward
1
arrow_downward

Нет, это было сделано для решения этой проблемы: https://github.com/Z3Prover/z3/issues. /1008

Команда ALLSAT не поддерживается z3; хотя было бы легко закодировать его, используя цикл «подтвердить отрицание предыдущей модели и перепроверить». Большинство высокоуровневых интерфейсов обеспечивают это как уровень поверх того, что возможно при использовании SMT-Lib2. Если вам нужна поддержка для этого, лучше сначала убедить разработчиков SMTLib (http://smtlib.cs.uiowa.edu/), поэтому будет разработан стандартный способ сделать это, и его можно будет реализовать с помощью нескольких решателей.

person alias    schedule 06.02.2018
comment
Я согласен с тем, что использование check-sat в цикле и возврат обратно инвертированной модели в качестве утверждения — это простой способ имитировать ALLSAT. Однако из моих результатов я вижу, что внутренняя стратегия сброса никоим образом не зависит от внешнего цикла. Было бы неплохо иметь хоть какое-то влияние извне. - person ChristianJ; 07.02.2018
comment
Кроме того, есть также вопросы о том, как all-sat должен вести себя при наличии квантификаторов. (Распространенная стратегия заключается в том, чтобы печатать только разные префиксы-экзистенциалы, и как только вы нажмете на все, оставьте все остальное в покое.) Но ни один из этих пунктов не является четко определенным или общепризнанным. Я думаю, что здесь есть место как для стандарта (например, SMTLib), чтобы установить основные ожидания, так и для инструмента (z3/yices и т. д.), чтобы реализовать то, как строится следующая модель, на которую вы намекаете. - person alias; 07.02.2018