Convert First-Order Logic to CNF

Question

I'm endeavouring to 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?

I'm sorry if I misunderstood your question, but I wonder if CNF have enough expressiveness for First order logic. For example "The brother of the father of any human(X) is his uncle (of X)" can be simply translated in first order logic. But (for what I remember of clauses) it seems to me that the clauses cannot express this generality (more precisely, the term "any human"). If I'm mistaken, then I'm sorry! — B. Decoster
No, @Fezvez, I think you're generally right, which is why I specified a discrete domain. For a variable with an infinite domain, there can be no well-formed CNF, since an infinite number of variables would be required. For a finite-domain, we can expand the anys and exists of first-order logic to make a (long) sequence of statements in predicate logic. — Richard

Alexander Serebrenik Alexander Serebrenik · Accepted Answer · 2012-03-26T19:06:54

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/

Convert First-Order Logic to CNF

1 Answers