Nice timing, I just finished it! I was able to adjust the bit mask format to be easier to work with by hand and got it most of the way, then used the SAT solver to quickly finish the rest when I got stuck.