Я пытаюсь использовать MiniSat для решения проблемы удовлетворения ограничений. В логике первого порядка проблема легко представляется несколькими переменными дискретной области и некоторыми предикатами.
Однако MiniSat, как и другие решатели CSP, которые я видел до сих пор, хотел бы, чтобы их ввод был в форме CNF. Итак, я ищу своего рода «препроцессор», который преобразует логические выражения первого порядка в CNF.
Есть предположения?
Возможно, вам понравится IDP3 от Katholieke Univ из Левена, Бельгия: http://dtai.cs.kuleuven.be/krr/software/idp3 IDP3 предлагает теории первого порядка (типизированная логика первого порядка с индуктивными определениями, агрегаты, ограниченная арифметика) и применяет minisat.
Другой вариант - Paradox от Koen Claessen (Chalmers U, Швеция). Paradox - это средство поиска конечных моделей для логики первого порядка, которое также начинается с преобразования в SAT, а затем решает формулу с помощью MiniSAT. Исходный код Paradox можно загрузить с http://www.cse.chalmers.se/~koen/code/
