# A generalized algorithm to convert a formula in algebraic normal form to an equivalent formula that minimizes the number of bitwise operations

In this question, “bitwise operation” means any operation from the set {XOR, AND, OR}. The NOT operation is not included because it can be represented as a single XOR with 1.

Given an arbitrary formula $$f$$ (in algebraic normal form), how to find an equivalent formula $$g$$ that minimizes the number of bitwise operations?

For example, assuming that $$x, y, z, u, v$$ are five bits, consider the following formula $$f$$ (to compute the bit $$w$$):

$$w = 1 \text{ XOR } (z \text{ AND } v) \text{ XOR } (x \text{ AND } v) \text{ XOR } u \text{ XOR } z \text{ XOR } (x \text{ AND } y) \text{ XOR } y \text{ XOR } x.$$

There are ten bitwise operations (XOR, AND) in this formula. But there exists a more compact formula $$g$$ to compute $$w$$:

$$w = 1 \text{ XOR } u \text{ XOR } (v \text{ OR } z) \text{ XOR } (x \text{ OR } (y \text{ XOR } v)).$$

Note that there are only six bitwise operations (XOR, OR) in this formula.

Is there an open-source program that allows to solve the problem? I have read this page in Sage Reference Manual, but I cannot find the relevant functionality there. I only found how to determine whether two formulas are equivalent:

import sage.logic.propcalc as propcalc
f = propcalc.formula("(z & v) ^ (x & v) ^ ~u ^ z ^ (x & y) ^ y ^ x")
g = propcalc.formula("~u ^ (v | z) ^ (x | (y ^ v))")
f.equivalent(g)


evaluates to True.

But how to obtain $$g$$ if only $$f$$ is given? What is a reasonably efficient (so I could apply it to a formula with up to five variables and obtain a solution in a reasonably short time) generalized algorithm that takes an arbitrary formula (in algebraic normal form) and outputs a formula with the minimal number of bitwise operations?