Есть ли способ использовать z3 для преобразования формулы в CNF (с использованием кодирования в стиле Цейцина)? Я ищу что-то вроде команды simplify, но гарантирую, что возвращаемая формула является CNF.
Преобразовать формулу в CNF
Ответы (1)
Для этого вы можете использовать команду apply. Мы можем предоставить этой команде произвольную тактику/стратегию. Дополнительную информацию о тактике и стратегиях в Z3 4.0 см. в руководстве http://rise4fun.com/Z3/tutorial/strategies
Команду (help-tactic) можно использовать для отображения всех доступных тактик в Z3 4.0 и их параметров. Программатик более удобен в использовании и гибок. Вот руководство, основанное на новом Python API: http://rise4fun.com/Z3Py/tutorial/strategies< /а>. Те же возможности доступны в API .Net и C/C++.
Следующий скрипт демонстрирует, как преобразовать формулу в CNF с помощью этой платформы:
person
Leonardo de Moura
schedule
12.06.2012
Большое спасибо! Это именно то, что я искал. Еще одно замечание: есть ли способ заставить z3 сообщить мне функцию, которую представляет каждая из новых переменных (k!0, k!1,...)? Или я должен реконструировать это из Цейтин-аксиом?
- person Georg; 12.06.2012
Нет, мы не предоставляем эту информацию. Однако Z3 создает преобразователь модели для каждого шага предварительной обработки. Преобразователь модели — это функция, которая преобразует модель результирующей формулы в модель исходной формулы. Для преобразования CNF конвертер моделей прост. Он просто удаляет интерпретацию новых переменных
k!0, k!1,... Таким образом, он не предоставляет нужной вам информации.
- person Leonardo de Moura; 13.06.2012
Хорошо, спасибо большое в любом случае. В любом случае восстановление функции для новых переменных из аксиом Цейтина кажется довольно простым.
- person Georg; 13.06.2012
@LeonardodeMoura Последняя ссылка не работает ;(
- person RexYuan; 13.11.2017
