Какой инструмент лучше всего конвертировать в CNF (или даже лучше в DIMACS CNF)?

Question

Я автоматически генерирую такие предложения с помощью программы на C ++:

((((((condition1#0 and not action1#0 and not action2#0 and TRUE) and (action1#1 and not action2#1 and not condition1#1 and TRUE) and TRUE)) or (not action1#0 and not action2#0 and not condition1#0 and action2#1 and not action1#1 and not condition1#1 and TRUE) or FALSE)))

Затем мне нужно проверить их соответствие с помощью какого-либо инструмента (например, MiniSat), но перед вводом их в таком инструменте мне нужночтобы конвертировать их в DIMACS CNF, знаете ли вы какой-нибудь инструмент, который может сделать это автоматически для меня?

Спасибо!

Редактировать :

Такжене-CNF Sat Solver будет работать нормально!

Answer 1

В pysmt есть анализатор, называемый читаемым человеком (hrparser), который должен иметь возможность анализировать эти выражения.[1].

Pysmt интегрирован как с picosat, так и с пакетом cudd bdd, так что вы можете легко проверить его на соответствие.В общем, решатели smt более гибки в структуре ввода (не cnf).Если вы можете изменить вывод кода c ++, может быть достаточно просто создать файл smtlib и использовать smt silver (например, yices, z3 или cvc4).

Примечание: я являюсь одним из разработчиков pysmt [1] http://pysmt.readthedocs.io/en/latest/_modules/pysmt/parsing.html#HRParser