Rewriting a boolean expression using different literals 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.
 A: 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.
