Sure, the SAT -> ILP is small but the reduction to SAT—or MILP directly—can sometimes (but not often) be large. Either way, I agree that there is likely some w

Sure, the SAT -> ILP is small but the reduction to SAT—or MILP directly—can sometimes (but not often) be large. Either way, I agree that there is likely some way in which the original commenter’s problem can be solved via MILP/MICP methods (indeed, I’ve found very few problems in practice that cannot be easily reduced) :)