Converting to Horn Form from CNF

1
votes

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.

1
prologsat-solvers
It might help if you defined what Horn form is and how it is different from the CNF format you're using, since CNF can be used to encode Horn formulas. - Kyle Jones
This does not make much sense imho. Being very informal: solving CNF is NP-hard, solving HornSat is in P. This means (using basic arguments by contradiction): complexity-wise, this transformation is as hard as solving the original CNF-SAT (NP-hard) and the output might be of exponential-size (not much you can do then with your HornSAT solver)! - sascha
Kyle Jones, how can CNF be used to encode Horn formulas? - piyo_kuro
sascha, so do you suggest me to just use in CNF - piyo_kuro
I don't suggest anything, but every good sat-solver works on cnf! Of course cnf can encode horn-formulas, as every horn-formula is a valid cnf (horn = much less powerful / much more constrained). 'What's unclear about the wiki article? - sascha

1 Answers

1
votes

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.