Simple logic synthesis using Z3: exercise from TAOCP

Found this exercise in TAOCP section 7.1.1 (Boolean basics):

I'm, not clever enough to solve this manually, but I could try using logic synthesis, as I did before. As they say, "machines should work; people should think".

My solutions for NAND, NAND with 0/1 constants, ANDN, ANDN with 0/1 constants.

Correct answers from TAOCP:

My solutions are slightly different: I haven't "pass through" instruction, so sometimes a value is copied from the input to the output using NAND/ANDN. Also, my versions are sometimes different, but correct and has the same length.

The modified Z3Py script.

→ [list of blog posts]

Please drop me email about any bug(s) and suggestion(s): dennis(@)