Конвертировать логику первого порядка в CNF

Question

Я пытаюсь использовать MiniSat для решения проблемы удовлетворения ограничений.В логике первого порядка проблема легко представляется несколькими дискретными переменными и некоторыми предикатами.

Однако MiniSat, наряду с другими решателями CSP, которые я видел до сих пор, хотел бы, чтобы их ввод вФорма CNF.Поэтому я нахожусь в поиске «препроцессора», который преобразует логические выражения первого порядка в CNF.

Есть мысли?

Answer 1

Возможно, вы захотите рассмотреть IDP3 из Katholieke Univ из Лёвена, Бельгия: http://dtai.cs.kuleuven.be/krr/software/idp3 IDP3 пропозиционирует теории первого порядка (типизированная логика первого порядка с индуктивными определениями, агрегатами, ограниченной арифметикой) и применяет минисат.

Другим вариантом будет Paradox от Koen Claessen (Chalmers U, Швеция). Paradox - это конечный искатель моделей для логики первого порядка, который также начинается с перевода в SAT, а затем решает формулу с помощью MiniSAT. Исходный код Paradox можно скачать с http://www.cse.chalmers.se/~koen/code/