Бележките по изданието за z3 версия 4.6 споменават нова функция „издаване на множество (check-sat) повиквания, докато не се върне обратно“. Това е еквивалент на ALLSAT?
Къде мога да намеря допълнителна документация или пример за тази функция?
издаване на множество (check-sat) повиквания, докато не се върне ненаселено
comment
Да, става дума за разговори за оптимизация. Не е свързано с AllSAT. Няма вграден метод за ALL-SAT.
- person Nikolaj Bjorner schedule 06.02.2018
Отговори (1)
Не, това беше за справяне с този проблем: https://github.com/Z3Prover/z3/issues/1008
Команда ALLSAT не се поддържа от z3; въпреки че би било лесно да го кодирате с помощта на цикъла "утвърждаване на отрицанието на предишния модел и повторна проверка". Повечето интерфейси на високо ниво предоставят това като слой върху това, което е възможно с помощта на SMT-Lib2. Ако искате поддръжка за това, може би е най-добре първо да убедите хората от SMTLib (http://smtlib.cs.uiowa.edu/), така че стандартен начин за това ще бъде разработен и може да бъде приложен от множество решаващи програми.
person
alias
schedule
06.02.2018
Съгласен съм, че използването на check-sat в цикъл и връщането обратно на отречения модел като твърдение е лесен начин за имитиране на ALLSAT. Въпреки това виждам от резултатите си, че вътрешната стратегия за нулиране по никакъв начин не се влияе от външния цикъл. Би било хубаво да има поне някакво влияние отвън.
- person ChristianJ; 07.02.2018
Освен това има и въпроси относно това как трябва да се държи all-sat в присъствието на квантификатори. (Обща стратегия е да отпечатате само различни екзистенциални префикси и след като ударите за всички, оставете всичко останало на мира.) Но нищо от това не е добре уточнено или общоприето. Мисля, че тук има място както за стандарта (т.е. SMTLib), за да зададете основните очаквания, така и за инструмента (z3/yices и т.н.), за да приложите как е конструиран следващият модел, както намеквате.
- person alias; 07.02.2018
