Comment by OutOfHere
2 days ago
The article fails to even say what SMT is. It also fails to describe and explain it. This article should help:
https://en.wikipedia.org/wiki/Satisfiability_modulo_theories
2 days ago
The article fails to even say what SMT is. It also fails to describe and explain it. This article should help:
https://en.wikipedia.org/wiki/Satisfiability_modulo_theories
In the article:
> "Satisfiability Modulo Theories"
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).
[flagged]
From the source for the page.