Comment by b0a04gl

you mentioned SMT is slower than SAT and left it there, but that feels incomplete. in problems like this, solve time barely matters unless you’re generating at scale. the real weight is in how fast you can write, refactor, and trust the constraints. SAT might give faster outputs, but SMT usually gets you to correct models quicker with less friction. wondering if you actually benchmarked both and stuck with SAT on numbers, or if it was more of a default comfort pick. felt like a missed moment to shift the lens from solver speed to model dev loop speed