[nextos]

Decoupling both is the simplest option, but not the one I am focusing on. Also note SAT/SMT can also be used for synthesis.

In fact, synthesis has a relatively rich history using SAT/SMT solvers.

[yaj54]

Are you using the SAT/SMT solvers to feed training data into a transformer or integrating the solver logic into the model code?