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