Есть ли инструмент, который реализует не-CNF SAT решатель?

Question

Мне нужен SAT-решатель, способный принимать в качестве входных данных не только файлы CNF, но и обычные текстовые файлы, содержащие предложения с предложениями (записанные только с и или и , а не ).

Я не смог найти ни одного.Не могли бы вы указать один?

Answer 1

После тщательного поиска я нашел limboole: http://fmv.jku.at/limboole/.

Это действительно полезно, поскольку оно принимает любую формулу логики высказываний и может вычислять, является ли она действительной или выполнимой.

Answer 2

Взгляните на bc2cnf , инструмент командной строки, который переводит логические «схемы» в CNF.

Схема - это коллекция булевых выражений.Выражения могут использоваться в качестве входных переменных для других выражений.

Получив CNF, вы можете передать его в SAT solver , например cryptominisat или Z3 , чтобы найти решения, которые удовлетворяют вашему выражению (ям).

Смотрите похожие сообщения: здесь и здесь