I use CP-SAT for automated design problems. I need a guarantee on solution quality, so gen AI is a nonstarter. The problem formulation is quite messy and has constraints that can vary by locale. CP-SAT handles it pretty well. The one thing I've been trying to model well are cover constraints where for each x : xs, there is some y : ys st. pred(x, y). I've tried both boolean matrices and index constraints, and they wo…
I’m not an expert here, but it sounds like you’re forcing a first-order logic problem into a propositional logic box.
A “native” first-order logic solver like Z3 might be something to try.