Comment by not2b

So just use a SAT solver to check for checking whether pattern matching is exhaustive. Any decent one will have much better performance than the current approach in the Rust compiler for complex cases. The interesting thing about SAT is that although the worst case is exponential (as far as we know until someone proves P = NP), even huge real-life problems (from circuits, program analysis etc) tend to have structure that makes them quickly solvable with a SAT solver. And if not, have a time budget and report "too complex to solve" if exceeded.