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.
Best Answer
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.