[abhgh]

I am yet to read up on xcc so this is helpful, thanks. One thing that I found useful as an application from Knuth's lecture (I'm not sure if it's edited out because it was an audience discussion, I attended the 2023 talk in person, reg. which I commented on another thread [1]), is that it can produce multiple SAT solutions, as opposed to just one,which seems to be the case now (definitely true for z3 which I have used a bit). This is important in practice because often there are downstream constraints which you might become aware of later (e.g., there're other hidden "soft" costs you didn't factor in), and because of which you now need to go back and need to run the solver again to find an alternative solution. This is time consuming but the worse part is there is no good way to avoid the first solution except by adding another constraint, e.g. original constraints + not(first solution).

Edit: as an extension of the above, the second solution mightn't work well too, in which case you'd need to repeat the above till you find a solution that you like. Very painful in practice.

[1] https://news.ycombinator.com/item?id=38775882