3 ms·

here's a cool example from somebody at Microsoft: https://medium.com/@ahelwer/checking-firewall-equivalence-with-z3-c2efe5051c8f https://medium.com/@ahelwer/ch

here's a cool example from somebody at Microsoft: https://medium.com/@ahelwer/checking-firewall-equivalence-with-z3-c2efe5051c8f 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 6y ago
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 https://en.wikipedia.org/wiki/Satisfiability_modulo_theories [1] https://news.ycombinator.com/item?id=23997128 https://news.ycombinator.com/item?id=23997128