as_addition.py

# https://twitter.com/geofflangdale/status/1798605087885214050

import inspect
import itertools

def sat(formula, preassignment, n=None):
	# just bruteforce it, but could be a sat solver too
	if n is None:
		n = len(inspect.getfullargspec(formula)[0])
	for inputs in itertools.product((0, 1), repeat=n):
		output = formula(*inputs)
		io = inputs + (output,)
		for index, value in preassignment:
			if io[index] != value:
				break
		else:
			return True
	return False

def decompose_as_addition(formula):
	lhs = ""
	rhs = ""
	xor = ""
	names = inspect.getfullargspec(formula)[0]
	n = len(names)
	remaining = list(enumerate(names))
	assign = []
	while remaining:
		#print("----", assign)
		if not sat(formula, assign + [(n, 0)]) or not sat(formula, assign + [(n, 1)]):
			# already fully determined
			break

		for i, name in remaining:
			imply0 = None
			if not sat(formula, assign + [(i, 0), (n, 0)]):
				imply0 = 1
			elif not sat(formula, assign + [(i, 0), (n, 1)]):
				imply0 = 0

			imply1 = None
			if not sat(formula, assign + [(i, 1), (n, 0)]):
				imply1 = 1
			elif not sat(formula, assign + [(i, 1), (n, 1)]):
				imply1 = 0

			#print("  ", i, name, imply0, imply1)

			swap = imply0 == 1 or imply1 == 0
			if swap:
				imply0, imply1 = imply1, imply0

			if (imply0, imply1) == (0, 1):
				lhs += name
				xor += "1" if swap else "0"
				rhs += "1"
				remaining = []
				break
			if imply0 == 0:
				lhs += name
				xor += "1" if swap else "0"
				rhs += "0"
				assign.append((i, 1^swap))
				remaining.remove((i, name))
				break
			elif imply1 == 1:
				lhs += name
				xor += "1" if swap else "0"
				rhs += "1"
				assign.append((i, 0^swap))
				remaining.remove((i, name))
				break

		else:
			raise Exception()

	if "1" in xor:
		return "(({} ^ {}) + {}) >> {}".format(lhs, xor, rhs, len(rhs))
	else:
		return "({} + {}) >> {}".format(lhs, rhs, len(rhs))

print("a & b & (c | d)  =", decompose_as_addition(lambda a, b, c, d: a and b and (c or d)))
print("(a | b) & c & d  =", decompose_as_addition(lambda a, b, c, d: (a or b) and c and d))
print("a & !b & (c | d) =", decompose_as_addition(lambda a, b, c, d: a and not b and (c or d)))
print("a & !(b | !c)    =", decompose_as_addition(lambda a, b, c: a and not (b or not c)))
print("a & (b | !b)     =", decompose_as_addition(lambda a, b: a and (b or not b)))

# a & b & (c | d)  = (abcd + 0011) >> 4
# (a | b) & c & d  = (cdab + 0011) >> 4
# a & !b & (c | d) = ((abcd ^ 0100) + 0011) >> 4
# a & !(b | !c)    = ((abc ^ 010) + 001) >> 3
# a & (b | !b)     = (a + 1) >> 1