Как преобразовать логическое выражение в файл cnf?

Question

Как преобразовать логическое выражение в файл cnf?

Мне нужно использовать Sat Solver для проверки выполнимости логических выражений..

У меня сложное логическое выражение, как это

альтернативный текст

Есть ли автоматический конвертер файлов CNF, так что я могу дать его прямо в Sat Solver?

Я прочитал файл формата cnf.. но как выразить это выражение в файле.cnf? я запутался, когда внутри парантеза есть соединение и как выразить -> и <->? Помогите мне, пожалуйста

4

java boolean-expression sat-solvers conjunctive-normal-form

Источник

user416123 16 окт '10 в 07:39

2 ответа

Решение

SBSAT - это основанный на состоянии SAT-решатель, который может принимать различные входные форматы. Вы можете взять простое выражение и передать его в SBSAT для преобразования в CNF. Руководство, раздел 4.10, описывает, как это сделать.

2

Источник

user14113 06 ноя '12 в 03:09

Другие вопросы по тегам java boolean-expression sat-solvers conjunctive-normal-form

user569266 17 янв '11 в 19:58 2011-01-17 19:58 · Accepted Answer · 2011-01-17 19:58

Есть несколько решений.

Limboole - это инструмент с открытым исходным кодом, который, как мне кажется, включает в себя отдельный конвертер "логика высказываний в CNF".

В более общем смысле вы также можете использовать инструмент, который изначально поддерживает логику высказываний; некоторые примеры включают Z3, CVC3 и Yices.