# Distributive expansion of CNF and implicants

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 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 to illustrate the effects.

• 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. Nov 30, 2013 at 21:53
• 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. Nov 30, 2013 at 22:51
• @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? Nov 30, 2013 at 23:42
• 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. Dec 1, 2013 at 2:53
• @VijayD The examples were removed by Kaveh not by me. Dec 1, 2013 at 8:58