Comment by rook37
2 days ago
Huh, where? I didn't see it going through and opening it in reader mode and ctrl+f-ing any of those words turns up nothing for me still.
2 days ago
Huh, where? I didn't see it going through and opening it in reader mode and ctrl+f-ing any of those words turns up nothing for me still.
He embeds the footnotes in the web version (it's a proper footnote in the email newsletter version). Find the "..." in this paragraph:
> Ryan solved this by writing Queens as a SAT problem, expressing properties like "there is exactly one queen in row 3" as a large number of boolean clauses. Go read his post, it's pretty cool. What leapt out to me was that he used CVC5, an SMT solver. (...) SMT solvers are "higher-level" than SAT, capable of handling more data types than just boolean variables. It's a lot easier to solve the problem at the SMT level than at the SAT level. To show this, I whipped up a short demo of solving the same problem in Z3 (via the Python API).