# Making iterative consensus optimal

The iterative consensus non-optimal as it will return terms that is covered by prime implicants. An example of this is $xp \lor x'q = xp \lor x'q \lor pq$ that cannot be absorbed. Here is a modified algorithm that adds polynomial complexity: $\blacksquare ~ \textnormal{\textbf{Algorithm} \emph{Optimal iterative consensus}}$

1. Let $\mathcal{L}_A$ and $\mathcal{L}_B$ be two disjoint list. The induction assumption is that $\mathcal{L}_A$ contain only essential terms.
2. For all pairs $(x,y) \in \mathcal{L}_A \cup \mathcal{L}_B$, calculate $z = cons(x,y)$. Place the resulting term $z$ in:
1. $\mathcal{L}_A \iff x \in \mathcal{L}_A \land deg(z) < deg(x) \lor y \in \mathcal{L}_A \land deg(z) < deg(y)$. Then perform absorption on $z, x, y$.
2. $\mathcal{L}_B$ otherwise.
3. For all pairs $(x,y) \in \mathcal{L}_A \cup \mathcal{L}_B$, perform absorption. If any absorbent is in $\mathcal{L}_A$, then the result is in $\mathcal{L}_A$.
4. If $\mathcal{L}_A \cap \mathcal{L}_B \neq \emptyset \implies \mathcal{L}_B = \mathcal{L}_A \backslash (\mathcal{L}_A \cap \mathcal{L}_B)$.
5. If no new terms appear in step 2 or 3, stop and output $\mathcal{L}_A$. Otherwise go to 2.

The proof of this being correct goes as follows: $\blacksquare ~ \textnormal{\textbf{Proposition}}$ If all terms in iteration $i$ are essential, then all terms in iteration $i+1$ are essential.

Proof. Consider the following steps:

1. We first show that no non-essential terms can be in in $\mathcal{L}_A$ after the $i$th iteration. Assume that we add a term $z'$ that is non-essential to $\mathcal{L}_A$. By 2.a, at least one of the consensus terms, let this be $x$ (wlog), yielding z′ must be essential. If $deg(z') < deg(x)$, then $z'$ must cover $x$. Now, $x$ is absorbed into $z'$. $z'$ is non-essential by assumption, but it is the only one covering the value that made $x$ essential. Contradiction.
2.  We now show that no essential terms are in $\mathcal{L}_B$. We proceed in the same manner by assuming that $z'$ is essential. Since $z' \in \mathcal{L}_B$, two cases appear: (a) it is a consensus of  two non-essential terms, which clearly not is essential or (b) one term is essential $x$ and one term is not $y$. If $deg(z') \geq deg(x)$, $z'$ can only cover a subset of $x$ and cannot be essential. $\blacksquare ~ \textnormal{\textbf{Lemma}}$ The algorithm presented above returns an optimal expression of any essential terms.

Proof. By the Induction axiom  in conjunction with the assumption that all initial terms were essential and Proposition 1, we see that $\mathcal{L}_A$ contains all essential terms at all iterations. Thus, it will contain all essential term at the end of the execution algorithm.

If you find a counterexample or an error in the steps of the proof, please report it!