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.

  • 1
    $\begingroup$ Write it in DNF (easy) and then use distributivity. $\endgroup$ – Emil Jeřábek Dec 1 '17 at 16:21
  • 1
    $\begingroup$ @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? $\endgroup$ – fedja Dec 1 '17 at 16:33
  • $\begingroup$ @fedja I have no idea what’s the point. Only the OP can answer that, don’t you think? $\endgroup$ – Emil Jeřábek Dec 1 '17 at 16:51
  • $\begingroup$ @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 :-) $\endgroup$ – fedja Dec 1 '17 at 17:00
  • $\begingroup$ 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. $\endgroup$ – user1747134 Dec 4 '17 at 9:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.