Добавление предложений непосредственно в решатель z3
У меня есть AIG (и -инверторный график), который я продолжаю модифицировать и чью удовлетворенность мне нужно проверять пошагово, используя Z3. Я могу сгенерировать представление AIG в формате CNF и в идеале хотел бы передать эти предложения непосредственно решателю и повторно вызывать его из моего кода. Есть ли какой-то способ, которым я могу напрямую добавлять предложения (или AIG) в решатель Z3 через API C / C ++?
Решение
Да, вы можете просто утверждать новые утверждения, которые внутренне переводятся в предложения.
Обратите внимание, что для многих задач поэтапного решения Z3 не использует готовый, специализированный SAT-решатель, но имеет собственный SMT-решатель, который включает в себя некоторые функции SAT-решателей, но не все, и который изначально обрабатывает небулевые проблемы. Таким образом, это не обязательно тот случай, когда взлом решателя для непосредственного введения предложений приведет к значительному повышению производительности.
У Z3 также есть специальный булевский SAT-решатель, и если вы решаете чисто булевы задачи, этот решатель, вероятно, будет намного быстрее. Вы можете заставить его использовать этот решатель, заменив (check-sat) с (check-sat-using sat)или запустив тактику под названием «сат». Реализация этого решателя находится в sat_solver.h / .cpp, это было бы лучшее место, чтобы начать осматриваться, если вы хотите взломать его.
Z3 также использует собственную реализацию AIG в качестве этапа предварительной обработки в некоторых тактиках, см. aig_tactic.h / .cpp.
Другие решения
Других решений пока нет …