[viraptor]

NP-hard is just a complexity class, not a minimal threshold. SAT solving is kind of a guided optimistic bruteforcing. If the example is small enough, you can still solve it very quickly. Same as you can solve travelling salesman for a small number of cities. We solve small cases of NP-hard things all over the place.

[viraptor]

(not to confirm it's an np-hard problem - it may not even be decidable generally, but in practice yes, you can check it that way and SMT2 theories provide the right ops)