What is the smallest 3-CNF system of equations possible that enforces the boolean expression: a = b + c for boolean variables a, b, c?

'Smallest' can be defined as: (1) Number of 3 CNF clauses. (2) Number of new variables introduced in the clauses.

We are interested in both cases.

  • $\begingroup$ What do you mean by $+$? XOR or disjunction? $\endgroup$ Jan 13 at 11:41
  • $\begingroup$ disjunction.... $\endgroup$
    – J.Doe
    Jan 13 at 12:15

1 Answer 1


To begin with, note that $b+c$ can be expressed as the disjunction $b\lor c$. To enforce equation, you need to express "$a$ iff $(b\lor c)$", and that can be encoded as the following CNF formula: $$ \phi = (\neg a \lor b \lor c) \wedge ((\neg b \wedge \neg c) \lor a)$$

Indeed, I used the fact that $A\to B \equiv \neg A \lor B$ and applied that twice. $\phi$ is not in CNF form, but you can simplify it to: $$ \phi = (\neg a \lor b \lor c) \wedge (\neg b \lor a) \wedge(\neg c \lor a) $$

Note that $\phi$ can be read as "c implies a, and b implies a, and a implies at least one of b or c". Can you prove that it is minimal?

  • $\begingroup$ aha. I think this works fine! thanks a lot. $\endgroup$
    – J.Doe
    Jan 13 at 11:17

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.