Convert First-Order Logic to CNF

I'm endeavouring t开发者_Go百科o use MiniSat to solve a constraint satisfaction problem. In first-order logic the problem is easily represented by a few discrete-domain variables and some predicates.

However, MiniSat, along with the other CSP solvers I've seen so far, would all like their input in CNF form. So I'm in search of a "preprocessor" of sorts which will convert first-order logic expressions into CNF.

Any thoughts?

You might like to consider IDP3 from Katholieke Univ of Leuven, Belgium: http://dtai.cs.kuleuven.be/krr/software/idp3 IDP3 propositionalises first-order theories (typed first order logic with inductive definitions, aggregates, bounded arithmetic) and applies minisat.

Another option would be Paradox from Koen Claessen (Chalmers U, Sweden). Paradox is a finite model finder for first order logic, that also starts by translating to SAT and then solves the formula using MiniSAT. The source code of Paradox can be downloaded from http://www.cse.chalmers.se/~koen/code/