prologsat-solvers

Converting to Horn Form from CNF


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.


Solution

  • 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.