# 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:

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.

• For just six input variables, a complete enumeration would be very fast. A truth table with 64 rows can easily be minimized by Espresso. – Axel Kemper Dec 9 '19 at 12:19
• Welcome to MSE Perceval, interesting question, but I suggest you to edit the it with Mathjax so its easier to read, see also MathJax basic tutorial and quick reference – user483923 Dec 9 '19 at 13:07
• @AxelKemper, you are right, I forgot to mention that the actual problem I'm facing involves up to 10 groups of 2 to 20 exclusive literals, so that the enumeration can grow quite large. I edited my question to state this, and added some clarifications. – Perceval W Dec 9 '19 at 19:24
• I can't tell, but do you want to use Tseytin transformation – user483923 Dec 12 '19 at 18:45

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.

• Thank you for your detailed answer. However as more "independent" variables (like A4) are added to the problem, I'm afraid that any SAT enumeration will become too slow (I plan to have more than 50 literals in my problem). Also, do you know a way to take the fact that F is true into account during the minimization process, such that y and z can be thrown away since (y OR z) is always true when (u and w) is true and F is true ? – Perceval W Dec 9 '19 at 19:16
• MiniZinc is capable to exploit shortcuts. A larger number of variables should also be no problem. However, if the number of solutions (minterms) is high, the subsequent Espresso run might be the hurdle. – Axel Kemper Dec 9 '19 at 21:22
• You might want to try bc2cnf together with a SAT solver like Z3 or cryptominisat. The problem remains the potential large number of solutions. – Axel Kemper Dec 9 '19 at 21:24