The pdf linked on this site is the biggest collection of SMT examples I know of: https://sat-smt.codes/ https://sat-smt.codes/ I’m no SMT expert, but the way I

The pdf linked on this site is the biggest collection of SMT examples I know of: https://sat-smt.codes/ https://sat-smt.codes/ I’m no SMT expert, but the way I’ve done it is to make some representation in Python Z3, and then write some function or class that generates those. I was solving MLB eliminations (more complex than it sounds) and I think I used arrays of ints for number of wins. So I’d pull MLB data, turn that into schedule objects which turned themselves into z3 constraints.