# Does this solve boolean satisfiability problem in polynomial time?

CNF can be easily converted into a formula that uses only AND and NOT operations, using the fact that a OR b = NOT(NOT(a) AND NOT(b)), in linear time.

This formula can be represented as a graph, where an edge goes down to T or F depending on whether that variable or intermediate node is ANDed without or with NOT: This problem can be further reduced to Horn satisfiability as the picture above shows, by using the fact that (x=>y) = NOT(x) OR y and introducing substitution variables so to satisfy the requirement for all clauses to be Horn clauses. In turn, Horn satisfiability can be solved in linear time.

So it seems that boolean satisfiability can be solved in linear time with this approach.

• Not all logic expressions can be captured by Horn Clauses Aug 15 '18 at 15:31

The general idea of reducing a more-or-less arbitrary expression to Horn clauses (without incurring exponential blowup) is highly suspect, since it turns a hard problem into a super-easy one. Indeed, I think you have miscalculated the effect of introducing the conditions $(\bar{a} \vee x_2)(a \vee \bar{x_2})$: this actually forces $a = x_2$, not $a = \bar{x_2}$. It makes sense that Horn clauses would not be able to express negation very well, since they express a certain type of monotonicity.