@mirth @regehr I do have some experience with combinatorial search, mostly when I was a student a couple decades ago, and I love it! In a way I think it's kind of disappointing that SMT solvers are so good, because they make it not worth learning search techniques for most problems unless you get extra deep into a problem, and that takes away some of the joy of studying search.