I am looking at Conjunctive Normal Form examples, such as this:

${\displaystyle (A\lor \neg B\lor \neg C)\land (\neg D\lor E\lor F)}$

where it is a conjunction (AND) of disjunctions (ORs). So it's an AND of ORs. That's coming from looking at Demorgan's Laws, such as these:

${\displaystyle \neg (P\land Q)\vdash (\neg P\lor \neg Q).}$

${\displaystyle \neg (P\lor Q)\vdash (\neg P\land \neg Q).}$

That is coming from looking at minimally functionally complete operator sets, such as these:

  • One element

    ${↑}, {↓}$

  • Two elements

    ${\displaystyle \{\vee ,\neg \}} {\displaystyle \{\vee ,\neg \}}, {\displaystyle \{\wedge ,\neg \}} {\displaystyle \{\wedge ,\neg \}}, {\displaystyle \{\to ,\neg \}} {\displaystyle \{\to ,\neg \}}, {\displaystyle \{\gets ,\neg \}} {\displaystyle \{\gets ,\neg \}}, {\displaystyle \{\to ,\bot \}} {\displaystyle \{\to ,\bot \}}, {\displaystyle \{\gets ,\bot \}} {\displaystyle \{\gets ,\bot \}}, {\displaystyle \{\to ,\nleftrightarrow \}} {\displaystyle \{\to ,\nleftrightarrow \}}, {\displaystyle \{\gets ,\nleftrightarrow \}} {\displaystyle \{\gets ,\nleftrightarrow \}}, {\displaystyle \{\to ,\nrightarrow \}} {\displaystyle \{\to ,\nrightarrow \}}, {\displaystyle \{\to ,\nleftarrow \}} {\displaystyle \{\to ,\nleftarrow \}}, {\displaystyle \{\gets ,\nrightarrow \}} {\displaystyle \{\gets ,\nrightarrow \}}, {\displaystyle \{\gets ,\nleftarrow \}} {\displaystyle \{\gets ,\nleftarrow \}}, {\displaystyle \{\nrightarrow ,\neg \}} {\displaystyle \{\nrightarrow ,\neg \}}, {\displaystyle \{\nleftarrow ,\neg \}} {\displaystyle \{\nleftarrow ,\neg \}}, {\displaystyle \{\nrightarrow ,\top \}} {\displaystyle \{\nrightarrow ,\top \}}, {\displaystyle \{\nleftarrow ,\top \}} {\displaystyle \{\nleftarrow ,\top \}}, {\displaystyle \{\nrightarrow ,\leftrightarrow \}} {\displaystyle \{\nrightarrow ,\leftrightarrow \}}, {\displaystyle \{\nleftarrow ,\leftrightarrow \}} {\displaystyle \{\nleftarrow ,\leftrightarrow \}}$

  • Three elements

    ${\displaystyle \{\lor ,\leftrightarrow ,\bot \}} {\displaystyle \{\lor ,\leftrightarrow ,\bot \}}, {\displaystyle \{\lor ,\leftrightarrow ,\nleftrightarrow \}} {\displaystyle \{\lor ,\leftrightarrow ,\nleftrightarrow \}}, {\displaystyle \{\lor ,\nleftrightarrow ,\top \}} {\displaystyle \{\lor ,\nleftrightarrow ,\top \}}, {\displaystyle \{\land ,\leftrightarrow ,\bot \}} {\displaystyle \{\land ,\leftrightarrow ,\bot \}}, {\displaystyle \{\land ,\leftrightarrow ,\nleftrightarrow \}} {\displaystyle \{\land ,\leftrightarrow ,\nleftrightarrow \}}, {\displaystyle \{\land ,\nleftrightarrow ,\top \}} {\displaystyle \{\land ,\nleftrightarrow ,\top \}}$

This got me wondering why you always see the CNF in automated theorem proving, if it can be simplified from it's 3 symbols to 2 symbols such as AND + NOT, or even one symbols such as NAND. So in my attempt at the CNF example above, it would become:

${\displaystyle \neg(\neg A\land (B\land C))\land \dots}$

...something like that...

I'm wondering what the downsides are to simplifying CNF into using only 2 operation types such as AND + NOT or OR + NOT. Along those lines, wondering what advantage CNF gives you over just using the corresponding two operation form. If you simplified a complex programmatic expression down to AND + NOT, I'm wondering if there would be any advantage to then "complexifying" that 2-operation form into the CNF's 3-operation form.

  • 1
    $\begingroup$ As you said two connectives (one of them : $\lnot$) are enough, and we can further shorten the list to one. Originally, normal form were used to check "mechanically" for validity : an expression in normal form is valid iff it has the characteristic that in each disjunction there occurs at least one of the elementary sentences together with its negation. $\endgroup$ – Mauro ALLEGRANZA Feb 5 '19 at 12:18

The first advantage lies within Horn clauses. If all your clauses are horn clauses, then there's an efficient way to find a minimal model which solves all clauses.

The second is that CNF/DNF isn't convoluted - you've got two layers, which is reasonably simple.

However, this simplicity comes with a price - CNF's/DNF's are for usual terribly long, so while in the DNF, you'd instantly get a model by simply searching for a clause that isn't impossible, transforming a formula into DNF is for usual already too time expensive.

So, what makes CNF better?
First, it naturally models multiple conjunctive requirements: Say you have the requirements $\phi \land \tau$. Then you simply have to create a CNF of both formulas $\phi,\tau$ individually to build the CNF of the whole formula.

Second, by introducing new variables $x_i$ one can greatly shorten a CNF by replacing all occurences of a formula $\tau$ with $x_i$ and afterwards adding a clause $x_i\Leftrightarrow \tau$. (One can even get by using only implications instead of equivalences).

So basically, the problem with DNF is that it's just too expensive to build, while CNF is both structurally easy and more or less affordable to build.

  • $\begingroup$ Awesome this is helpful. Wondering if you could explain briefly why you shouldn't just use the 2-operation form of AND + NOT instead of CNF, if there's anything other than just that it's more layers. $\endgroup$ – Lance Pollard Feb 5 '19 at 14:04
  • 1
    $\begingroup$ @LancePollard Unluckily, none of the text books I know of went that strongly in-depth. If you find any sources treating NOT+AND and its use for satisfiability tests, I'd be interested though. Otherwise I'd just guess that that if we use NOT+AND, we have some clauses we have to make true, and some we have to make false, and this additional trouble (compared to just having to make all/one clause true) simply isn't worth the effort. $\endgroup$ – Sudix Feb 5 '19 at 14:38

Well, the DNF has some advantages.

First, if you know that a combination of Boolean variables gives the value 1 (true), then there is a term in the DNF. E.g., if $f(A,\bar B)=1$, the contributing term is $A\wedge \bar B$.

Second, you can compare two Boolean functions by looking at their DNFs. If the DNFs are the same, the Boolean functions coincide.


Your Answer

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

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