A CNF formula is Horn-renamable if you can invert variables in such a way that each clause has at most one positive literal. There is an algorithm based on a reduction to 2-SAT given in Renaming a Set of Clauses as a Horn Set.

It seems, however, that by applying the standard reduction from CNF to 3-CNF, one could achieve a more efficient Horn-renaming algorithm. Consider a clause $(x_1\lor x_2\lor x_3\lor x_4)$ and its reduction $\color{blue}{(x_1\lor x_2\lor y_1)}\land\color{red}{(\overline{y_1}\lor x_3\lor x_4)}$. The former transforms into: $$(\overline{x_1}\lor\overline{x_2})\land(\overline{x_1}\lor\overline{x_3})\land(\overline{x_1}\lor\overline{x_4})\land(\overline{x_2}\lor\overline{x_3})\land(\overline{x_2}\lor\overline{x_4})\land(\overline{x_3}\lor\overline{x_4})$$

And the latter transforms into:


In this particular example the amount of clauses is equal, but consider a clause with $k$ variables. Without the reduction, there would be $\frac k 2\cdot(k-1)$ generated clauses. With the reduction there would be $(k-2)\cdot3$ generated clauses. I.e. without the reduction the growth is quadratic and with the reduction it's linear.

Given that the pigeonhole principle CNF encodings also use the same construction, this also gives a shorter way to write them.

However, is there any mention of this seemingly trivial relation in literature?



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.