41–42 of 42 posts
Earlier quoted context omitted.
Going one abstraction deeper, SAT solvers are black magic.
Yes, explaining the "why / how did the SAT solver produce this answer?" can be more challenging than explaining some machine learning model outputs. You can literally watch as the excitement and faith of the execs happens when the issue of explainability arises, as blaming the solver is not sufficient to save their own hides. I've seen it hit a dead end at multiple $bigcos this way.
Earlier quoted context omitted.
I guess z3 is fine with it, but it confuses me that they decided pips wouldn't have unique solutions
I actually wasn't aware of this either. Z3 is fine with it--its job is to find any satisfying model. The possible outcomes are "the puzzle is solvable and here's a solution" or "the puzzle isn't solvable."
For example, in https://zayenz.se/blog/post/benchmarking-linkedin-queens/#te... I took a large number of LinkedIn Queens puzzles, and I filtered out the ones that were not well-formed so that they wouldn't mess up the benchmarking and statistics.