You can simplify most of those problems by writing the constraints down in conjunctive/disjunctive normal forms and applying standard simplification on them, like you're back in school. That also eliminates things like repetition, since doing so also makes the problem declarative. If you need the recursive loops, you're guaranteed to be to stratify them for any reasonable problem. If you wanted, you could solve the problem optimally from this point by finding the prime implicants, or just accept a suboptimal solution that runs faster than you have any reason to care about, like datalog and sql do.
That doesn't work in general for mathematica because it's too powerful.
Even for boolean logic problems, a minimum-size CNF or DNF will not necessarily be the cheapest solution in terms of gates. As far as I know, hardly anyone has even attempted automatic minimization in terms of general binary operators.
That's true, it'll just be the minimal solution in SOP. I'm willing to call that good enough. My experience is that in practice you're often better off just relying on the fact that modern computers can execute billions of them per second.