# Converting complicated general propositional formula to CNF

I have a propositional formula of the form

$$\bigvee_{i=1}^n \neg \left( x_i \Leftrightarrow \left(\bigvee_{j=1}^{f(i)} y_{ij} \right) \right)$$

where the $x_i$'s are propositional variables and the $y_{ij}$'s are propositional literals (i.e., propositional variables or their negation) and $f : \mathbb{N} \to \mathbb{N}$ is just a function.

I would like to have this formula in Conjunctive Normal Form (CNF) using these general symbols.

The leading "quantifer" is a disjunction and I do not know how to change it to a conjunction in an efficient manner. Of course, it can be done manually for each specific instance, but that is very slow even on a computer.

• Write it in DNF (easy) and then use distributivity. – Emil Jeřábek Dec 1 '17 at 16:21
• @EmilJeřábek Getting $\prod_i 2^{f(i)}(f(i)+1)$ terms. Well, a few of them simplify by the rule $u\vee\neg u=\operatorname{true}$, but when I see such long expressions, my first instinct is to ask "What's the point?". So, one can do it, no problem, but what is the ultimate purpose of this exercise? – fedja Dec 1 '17 at 16:33
• @fedja I have no idea what’s the point. Only the OP can answer that, don’t you think? – Emil Jeřábek Dec 1 '17 at 16:51
• @EmilJeřábek Sure. It is just the damn restriction that you cannot put two "at"s in one remark. The last question is obviously addressed to the OP :-) – fedja Dec 1 '17 at 17:00
• The point to represent it in CNF is to be able to put as a constraint into a SAT solver. I see how it can be transformed to DNF, but I am not sure how to use distributivity while keeping the general form. – user1747134 Dec 4 '17 at 9:52