With an example: https://gist.github.com/adsharma/45fbb065a8fe793030e8360daebffba1 https://gist.github.com/adsharma/45fbb065a8fe793030e8360daeb... You could ha

With an example: https://gist.github.com/adsharma/45fbb065a8fe793030e8360daebffba1 https://gist.github.com/adsharma/45fbb065a8fe793030e8360daeb... You could have a puzzle that's described in plain English. I think the current day tech is sufficient to translate the puzzle to a python constraint like in this gist. The argument is that the SMT solvers are a better match for solving these problems than expensive matrix multiplication paid for by someone else. Of course, SMT is not a solution for every situation that Wolfram language is used for today. But a lot of the reasoning benchmarks fall in this category.