very generally speaking, are current SMT or SAT solvers about as efficient as dedicated solvers for NP hard problems, if you have some reasonable reduction from your problem space - or is all-custom typically the way to go?