[sobellian]

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 work but seem to be quite taxing on the solver. Maybe there's a better formulation.

[ibejoeb]

Is it a geometric problem, like every point must reside within the plane? Are you optimizing also, like finding the smallest bounding box that includes the most points? You can usually express these as global constraints, like non-overlapping intervals, or you can use these to precompute feasible candidates rather than manually encoding giant matrices that contain knowable bad values.

[sobellian]

It is a geometric problem. I do have no-overlap constraints, but the cover constraints relate to topology and scheduling. High level, I am taking a rectangle and generating a set of guillotine cuts. I have a list of locations that must lie on a guillotine cut. Some locations are known a priori, some are optimization variables. I have a hierarchical objective which in the end includes minimizing #cuts and material (length of each cut x a density associated with each cut according to several constraints).

[jkaptur]

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.