here's a cool example from somebody at Microsoft: https://medium.com/@ahelwer/ch... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		currymj on July 30, 2020 \| parent \| context \| favorite \| on: Kissat SAT Solver here's a cool example from somebody at Microsoft: https://medium.com/@ahelwer/checking-firewall-equivalence-wi... it's not a pure SAT problem, but Z3 works (in a way I don't understand) by reducing constraint problems involving integers and even more complicated domains into SAT problems.

MaxBarraclough on July 30, 2020 [–]

SMT solvers [0] like Z3 are very powerful things. They're used to power deductive software verification tools. We're discussing one such at [1].

[0] https://en.wikipedia.org/wiki/Satisfiability_modulo_theories

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

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact