<p>Theorem 1 is related to <a href="https://en.wikipedia.org/wiki/Blake_canonical_form" rel="nofollow">Blake canonical form</a>.</p>

<p>The Wikipedia article refers to</p>

<ul>
<li><em>Brown, Frank Markham, Boolean Reasoning: The Logic of Boolean Equations</em>,</li>
</ul>

<p>which in turn references</p>

<ul>
<li><em>Canonical expressions in Boolean algebra. Ph.D. dissertation U (1937)</em>).</li>
</ul>

CC BY-SA 3.0
2013-12-09T21:39:00.933Z
2013-12-09T21:39:00.933Z
wolfmanx
<p>I am looking for references for the following theorems.</p>

<p><strong>Theorem 1</strong>: Distributive expansion of a CNF formula $P_c$ (product of sums)
results in a DNF formula (sum of products) consisting of all prime
implicants for $P_c$. $P_c$ is called a Blake canonical form BCF.</p>

<p><strong>Theorem 2</strong>: If we transform a disjunctive clause $C_d$ with $k$ literals to a
disjunctive clause of conjunctions $C_m$ by replacing each literal
$l_i, i = (1, ..., k)$ with the conjunction $(\neg l_1 \wedge
... \wedge \neg l_{i-1} \wedge l_i)$, then $C_m$ will be logically equivalent to $C_d$. The clause $C_m$ is called a
clause with maximized conflicts.</p>

<p>Distributive expansion of $C_m$ shows that it is logically
equivalent to the unmaximized clause $C_d$, $C_m = C_d$.</p>

<p><strong>Theorem 3</strong>: Distributive expansion of a CNF formula with maximized conflicts
$P_m$ (product of sums of products), with simplification of
outermost clauses <em>before</em> innermost clauses, results in a DNF
formula $P_u$ (sum of products) defining a set of (not
necessarily prime) implicants $I_u$ for $P_m$. The
implicants from $I_u$ cover all possible solutions for
$P_m$.  The implicants $I_u$ are unique, in that no
implicant $M_i \in I_u$ covers the solutions of any other
implicant $M_j \in I_u, i \ne j$.</p>

<p><strong>Motivation</strong>:</p>

<p>With the discussion in [BROWN] I have finally found the last
piece of the puzzle.</p>

<p>Obviously, the restrictions for syllogistic formulae --- namely
removal of duplicate literals and elimination of clauses with
contradictory literals --- have been loosened over time. However, this
seems to have been a process of ad hoc reasoning.</p>

<p>I am missing an exhaustive formal discussion of the
consequences. I.e., the set of logically equivalent DNFs
represented by their minimal form of a disjunction of "atomic"
literals and the influence on the resulting DNFs of partial
assignments, which always cover all possible solutions, albeit in
different ways.</p>

<p>In order to find out, whether I have to do all of that on my own,
I use theorem 3 to show, that besides the well-known Blake canonical
form BCF, other non-trivial DNFs of implicants with different
properties appear, when the input clauses are generalized from
CNF to allow non-syllogistic representations, namely the DNFs
from theorem 2. Since that also requires a different order of
evaluation which is highly non-intuitive to simplification
junkies, I assume that I am out of luck.</p>

<p>It can especially be shown that for selection problems in "direct
encoding" (Chapter 2, <em>Handbook of Satisfiability</em>), the input based on theorem 2 alone allows a <a href="http://sw-amt.ws/satoku/doc/doc-experiments/README.html" rel="nofollow">CDCL solver to solve the problem with
significantly less decisions</a> than with plain CNF. Small problems
(currently 40 variables, 171 clauses) are even solved earlier with the
generally less effective "direct encoding" than with the original CNF
encoding. Note, that there is actually never a set of implicants
generated in that case.</p>

<p>I have prepared a <a href="http://sw-amt.ws/satoku/doc/doc-cnf-cdf-pde/satoku-cnf-cdf-pde.pdf" rel="nofollow">PDF with examples</a> to illustrate the effects.</p>

CC BY-SA 3.0
2013-11-30T21:53:48.603Z
What is the claim being made in Theorem 2? Is it that the two formulae are equivalent? Also, look at CDNF, which is used in the learning theory literature.
Vijay D
CC BY-SA 3.0
2013-11-30T22:51:15.783Z
Theorem 2 claims that the formulae are logically equivalent, i.e. in the fully expanded truth table they have the same entries set to true. I can add that, if necessary. The equivalence is $(p \vee q) = (p \vee (\neg p \wedge q))$, as given in the proof concept above. My stepson just told me, that I should not use  $\mapsto$. I will fix that.
wolfmanx
CC BY-SA 3.0
2013-11-30T23:42:52.483Z
@VijayD I assume CDNF = canonical disjunctive normal form? What is the relation to the theorems? It does not appear anywhere. I still hope that I find somebody to produce a correct formulation of my insights that finds mercy in the eyes of mathematicians. But I do have improved, haven't I?
wolfmanx
CC BY-SA 3.0
2013-12-01T02:53:29.740Z
Your use of $\mapsto$ was fine. The examples were helpful -- you could have left them. About CDNF, I meant conjunctions of DNF. Don't worry about the writing; it's fine. Also, I realised that the notion of "autarky" might be helpful for you.
Vijay D
CC BY-SA 3.0
2013-12-01T08:58:29.230Z
@VijayD The examples were removed by Kaveh not by me.
wolfmanx
CC BY-SA 3.0
2013-12-01T09:36:54.190Z
@VijayD Conjunctions of DNF are the natural input of my algorithm. "Autarky" was already pointed out by 
András Salamon for my question about "reliable assignments" [http://cstheory.stackexchange.com/questions/19626/questions-about-special-types-of-partial-assignments#comment52065_19739]. It's too loosely defined.
wolfmanx
CC BY-SA 3.0
2013-12-01T16:13:35.920Z
@VijayD I have finally found an adequate expression for what I need to know (see *motivation*).
wolfmanx
CC BY-SA 3.0
2013-12-09T13:53:44.347Z
Please post their references _as an answer_, instead of modifying the question.
Jeffε
<lo.logic><big-picture>
Distributive expansion of CNF and implicants
wolfmanx
# Distributive expansion of CNF and implicants

(Asked by: username_0 on 2013-11-29)

I am looking for references for the following theorems.

**Theorem 1**: Distributive expansion of a CNF formula $P\_c$ (product of sums)
results in a DNF formula (sum of products) consisting of all prime
implicants for $P\_c$. $P\_c$ is called a Blake canonical form BCF.

**Theorem 2**: If we transform a disjunctive clause $C\_d$ with $k$ literals to a
disjunctive clause of conjunctions $C\_m$ by replacing each literal
$l\_i, i = (1, ..., k)$ with the conjunction $(\neg l\_1 \wedge
... \wedge \neg l\_{i-1} \wedge l\_i)$, then $C\_m$ will be logically equivalent to $C\_d$. The clause $C\_m$ is called a
clause with maximized conflicts.

Distributive expansion of $C\_m$ shows that it is logically
equivalent to the unmaximized clause $C\_d$, $C\_m = C\_d$.

**Theorem 3**: Distributive expansion of a CNF formula with maximized conflicts
$P\_m$ (product of sums of products), with simplification of
outermost clauses *before* innermost clauses, results in a DNF
formula $P\_u$ (sum of products) defining a set of (not
necessarily prime) implicants $I\_u$ for $P\_m$. The
implicants from $I\_u$ cover all possible solutions for
$P\_m$. The implicants $I\_u$ are unique, in that no
implicant $M\_i \in I\_u$ covers the solutions of any other
implicant $M\_j \in I\_u, i \ne j$.

**Motivation**:

With the discussion in [BROWN] I have finally found the last
piece of the puzzle.

Obviously, the restrictions for syllogistic formulae --- namely
removal of duplicate literals and elimination of clauses with
contradictory literals --- have been loosened over time. However, this
seems to have been a process of ad hoc reasoning.

I am missing an exhaustive formal discussion of the
consequences. I.e., the set of logically equivalent DNFs
represented by their minimal form of a disjunction of "atomic"
literals and the influence on the resulting DNFs of partial
assignments, which always cover all possible solutions, albeit in
different ways.

In order to find out, whether I have to do all of that on my own,
I use theorem 3 to show, that besides the well-known Blake canonical
form BCF, other non-trivial DNFs of implicants with different
properties appear, when the input clauses are generalized from
CNF to allow non-syllogistic representations, namely the DNFs
from theorem 2. Since that also requires a different order of
evaluation which is highly non-intuitive to simplification
junkies, I assume that I am out of luck.

It can especially be shown that for selection problems in "direct
encoding" (Chapter 2, *Handbook of Satisfiability*), the input based on theorem 2 alone allows a [CDCL solver to solve the problem with
significantly less decisions](http://sw-amt.ws/satoku/doc/doc-experiments/README.html) than with plain CNF. Small problems
(currently 40 variables, 171 clauses) are even solved earlier with the
generally less effective "direct encoding" than with the original CNF
encoding. Note, that there is actually never a set of implicants
generated in that case.

I have prepared a [PDF with examples](http://sw-amt.ws/satoku/doc/doc-cnf-cdf-pde/satoku-cnf-cdf-pde.pdf) to illustrate the effects.

**Tags:** lo.logic, big-picture
> **Comments:**
> **username_1**: What is the claim being made in Theorem 2? Is it that the two formulae are equivalent? Also, look at CDNF, which is used in the learning theory literature.  
> **username_0**: Theorem 2 claims that the formulae are logically equivalent, i.e. in the fully expanded truth table they have the same entries set to true. I can add that, if necessary. The equivalence is $(p \vee q) = (p \vee (\neg p \wedge q))$, as given in the proof concept above. My stepson just told me, that I should not use  $\mapsto$. I will fix that.  
> **username_0**: @VijayD I assume CDNF = canonical disjunctive normal form? What is the relation to the theorems? It does not appear anywhere. I still hope that I find somebody to produce a correct formulation of my insights that finds mercy in the eyes of mathematicians. But I do have improved, haven't I?  
> **username_1**: Your use of $\mapsto$ was fine. The examples were helpful -- you could have left them. About CDNF, I meant conjunctions of DNF. Don't worry about the writing; it's fine. Also, I realised that the notion of "autarky" might be helpful for you.  
> **username_0**: @VijayD The examples were removed by Kaveh not by me.  
> **username_0**: @VijayD Conjunctions of DNF are the natural input of my algorithm. "Autarky" was already pointed out by  András Salamon for my question about "reliable assignments" [http://cstheory.stackexchange.com/questions/19626/questions-about-special-types-of-partial-assignments#comment52065_19739]. It's too loosely defined.  
> **username_0**: @VijayD I have finally found an adequate expression for what I need to know (see *motivation*).  
> **username_2**: Please post their references _as an answer_, instead of modifying the question.  

---

## 1 answers

### Answer by username_0 on 2013-12-09. Score: 1

Theorem 1 is related to [Blake canonical form](https://en.wikipedia.org/wiki/Blake_canonical_form).

The Wikipedia article refers to

* *Brown, Frank Markham, Boolean Reasoning: The Logic of Boolean Equations*,

which in turn references

* *Canonical expressions in Boolean algebra. Ph.D. dissertation U (1937)*).


---

