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))")

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?



You must log in to answer this question.