Once, when I was taking a music theory class, I tried to use the Z3 constraint solver to automatically harmonize melodies… it worked surprisingly well! https://github.com/kach/recreational-rosette/tree/master/mus...