One data problem boiled down to being an instance of the set cover problem (https://en.m.wikipedia.org/wiki/Set_cover_problem). Pretty easy to pose as an integer constraint problem, and Z3 solved it in about 20 minutes for me.