I'd like to implement an algorithm to rewrite a boolean expression as a sum of products of different boolean expressions (expressed as new literals).
Example
Let's say that I have some literals $A_0, A_1, A_2, A_3, A_4$ and an expression $F$ that should stay true: \begin{align} F = \text{exactly_one}(A_0, A_1, A_2, A_3) \end{align}
And I have some new literals, defined by
\begin{align}
\text{mapping}\ =\ &u \Leftrightarrow (A_0 \lor A_1)\ \land \\
&v \Leftrightarrow (A_2 \lor A_3)\ \land \\
&w \Leftrightarrow (A_0 \lor A_2)\ \land \\
&x \Leftrightarrow (A_1 \lor A_3)\ \land \\
&y \Leftrightarrow (A_0 \land A_5)\ \land \\
&z \Leftrightarrow (A_0 \land \neg A_5) \\
\end{align}
I'd like to represent $A_0 \lor A_3$ as a sum of products of the new literals.
For this example, two of the answers are:
$$A_0 \lor A_3 = (u \land w) \lor (v \land x)$$
$$A_0 \lor A_3 = y \lor z \lor (v \land x)$$
Preliminary thoughts
Iterating over all combinations of the new literals could be an answer but I suspect there is a more efficient way to solve the problem.
Another solution could be to enumerate all satisfying assignements of $u, v, w, x, y, z$ by solving the SAT problem
\begin{align} F \land (A_0 \lor A_3)\ &\land \\ (u \Leftrightarrow A_0 \lor A_1)\ &\land \\ (v \Leftrightarrow A_2 \lor A_3)\ &\land \\ (w \Leftrightarrow A_0 \lor A_2)\ &\land \\ (x \Leftrightarrow A_1 \lor A_3)\ &\land \\ (y \Leftrightarrow A_0 \land A_5)\ &\land \\ (z \Leftrightarrow A_0 \land \neg A_5)\ &\\ \end{align}
and then applying a SOP form minimizer like the Quines-McCluskey or Espresso algorithms, on the enumerated minterms. However, as the list of satisfying assignements can become exponentially long in the general case, it is not a viable approach.
Any idea is welcome.
EDIT
The example is misleading in the sense that:
- I want to handle many more variables (up to 10 groups of 2 to 10 exclusive expressions), so any enumeration can become intractable
- I'd like to take $F$ into account during the minimization of the formula, so that many simplications can be done
Another way to state the problem in a formal way is
Minimize the expression $\psi$ composed of the new literals ($u, v, w, x, y, z$), such that the following expression is always true $$ (A_0 \lor A_3) \land F\ \Leftrightarrow\ \psi \land \text{mapping} \land F $$
Another better example would be: given the expression \begin{align} F =\ &\text{exactly_one}(A_0, A_1, A_2, A_3)\ \land\\ &\text{exactly_one}(B_0, B_1)\ \land \\ &\text{one_or_none}(C_0, C_1)\ \land\ ((A_0 \lor A_3) \Leftrightarrow (C_0 \lor C1)) \\ \end{align}
that is, as a decision tree: choose between one of the $A_s$, and between one of the $B_s$ and if $A_0$ or $A_3$ is true, choose between $C_0$ or $C_1$.
and the new literals: \begin{align} \text{mapping}\ =\ &u \Leftrightarrow (A_0 \lor A_1) \land \\ &v \Leftrightarrow (A_2 \lor A_3)\ \land \\ &w \Leftrightarrow (A_0 \lor A_2)\ \land \\ &x \Leftrightarrow (A_1 \lor A_3)\ \land \\ &y \Leftrightarrow B_0\ \land \\ &z \Leftrightarrow B_1\ \land \\ &\alpha \Leftrightarrow C_0\ \land \\ &\beta \Leftrightarrow C_1 \end{align}
we wish to rewrite $A_0 \lor A_3$, ie minimize $\psi$ composed of the new literals such that the following expression is always true $$(A_0 \lor A3) \land F\ \Leftrightarrow \ \psi \land \text{mapping} \land F$$
Here, two solutions are: \begin{align} \psi &= (u \land w) \lor (v \land x) \\ \psi &= (\alpha \land \beta) \lor (v \land x) \end{align} But enumerating valid assignements of $u, v, w, x, y, z, \alpha, \beta$ can become intractable as we add more "independent" variables (that are not involved in the truthness of $A_0 \lor A_3$) like $y \Leftrightarrow B_0$ and $z \Leftrightarrow B_1$, and current logic minimizers do not allow to take F into account: we can get rid of $y$ and $z$ in the final solutions since F guarantees that one of them will always be true.
64
rows can easily be minimized byEspresso
. $\endgroup$