[0cf8612b2e1e]

I have only ever used Z3, but you might be onto something. Modeling problems is really challenging. It does not help that if you search for documentation or guidance there one two types of resources: beginner Sudoku or primary literature academic papers discussing the minutia of optimization properties with so much jargon.