How do you convert a CNF clauses to a Horn form using Prolog? I am trying to create a SAT Solver that has CNF as an input, which will be need to convert to Horn form.
Horn clauses are a subset of CNF. Namely CNF can be viewed as conjunction of general clauses, where every clause has the following form and where Ai,Bk are propositional variables and n>=0 and m>=0:
A1 v .. v An v ~B1 v .. v ~Bm
The Ai are the positive literals and the ~Bk are the negative literals. Horn clauses are now those general clauses which have in maximum one positive literal, i.e. n=<1. Namely which are of either of the form as follows:
A1 v ~B1 v .. v ~Bm
~B1 v .. v ~Bm
Now its impossible to convert every CNF into Horn Clauses, even if we would allow changing the sign of a literal in the representation. Take this formula nae(A,B,C)=(A xor B) v (B xor C) and the relevant sign changing variants as CNF:
nae(A,B,C) = (~A v ~B v ~C) & (A v B v C)
nae(A,B,~C) = (~A v ~B v C) & (A v B v ~C)
nae(A,~B,C) = (~A v B v ~C) & (A v ~B v C)
nae(A,~B,~C) = (~A v B v C) & (A v ~B v ~C)
nae(~A,B,C) = (~A v B v C) & (A v ~B v ~C)
nae(~A,B,~C) = (~A v B v ~C) & (A v ~B v C)
nae(~A,~B,C) = (~A v ~B v C) & (A v B v ~C)
nae(~A,~B,~C) = (~A v ~B v ~C) & (A v B v C)
They are all non-Horn Clauses so a renaming translation is not possible. But maybe using other reductions, possibly non-polynomial ones, can be used to translate CNF to Horn Clauses.
P.S.: The nae(A,B,C) example is taken from here.