4 ms·
In the article: > "Satisfiability Modulo Theories"
by Jtsummers 1y ago
In the article:
> "Satisfiability Modulo Theories"
- rook37 1y agoHuh, 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.
- Jtsummers 1y agoHe 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).
- OutOfHere 1y ago[flagged]
- Jtsummers 1y ago<p>"Satisfiability Modulo Theories" <a class="footnote-backref" href="#fnref:SMT" title="Jump back to footnote 2 in the text">↩</a></p> From the source for the page.