Rewriting a boolean expression using different literals

Question

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:

1. I want to handle many more variables (up to 10 groups of 2 to 10 exclusive expressions), so any enumeration can become intractable
2. 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.

Answer 1

I used MiniZinc to derive a truth-table for your example.

My model:

var bool: A0;
var bool: A1;
var bool: A2;
var bool: A3;
var bool: A4;
var bool: u;
var bool: v;
var bool: w;
var bool: x;
var bool: y;
var bool: z;

constraint sum([A0, A1, A2, A3]) == 1;

constraint u == (A0 \/ A1);
constraint v == (A2 \/ A3);
constraint w == (A0 \/ A2);
constraint x == (A1 \/ A3);
constraint y == (A0 /\ A4);   %  A5 replaced by A4
constraint z == (A0 /\ (not A4));

constraint A0 \/ A3;

output [" u v w x y z \n" ++ 
        show_int(2, u) ++ show_int(2, v) ++ 
        show_int(2, w) ++ show_int(2, x) ++ 
        show_int(2, y) ++ show_int(2, z)];

The resulting table:

 u v w x y z 
 0 1 0 1 0 0
-------------
 u v w x y z 
 1 0 1 0 1 0
-------------
 u v w x y z 
 1 0 1 0 0 1

Note that I replaced A5 by A4.

---

Another solution using Logic Friday 1:

Input function equation:

F = ((A0 & A1' & A2' & A3') | (A0' & A1 & A2' & A3') | 
     (A0' & A1' & A2 & A3') | (A0' & A1' & A2' & A3)) &
    (u == (A0 | A1)) & (v == (A2 | A3)) & 
    (w == (A0 | A2)) & (x == (A1 | A3)) & 
    (y == (A0 & A4)) & (z == (A0 & A4')) & 
    (A0 | A3);

Minimized:

F = A0' A1' A2' A3 u' v w' x y' z' 
  + A0 A1' A2' A3' u v' w x' y' A4' z 
  + A0 A1' A2' A3' u v' w x' y A4 z';

Resulting minimized table:

Internally, Logic Friday 1 is using Espresso to simplify truth-tables.