Formal methods are a cool way to verify that your hardware or software is working as intended™
Z3 is a one stop shop for FM with theorem proving, SAT, SMT, and computer algebra capabilities.
Let's look at some fun examples
👇
1/6
A nice usage is constraint solving for non-linear polynomial equations.
2/6
It can prove theorems or provide counter-examples!
3/6
Need to write a package manager and are pulling your hair out from dependency management? Don't worry!
Just create two simple functions that calculate dependencies and conflicts and solve!
This showcases that you can verify many arbitrary software behaviours as well.
4/6
It works with numpy! Here's an example solving an inverse kinematics equation for robotics!!
5/6
And the grand finalé! In just a few lines of code you can solve the infamous 8-queens problem by setting row, column, and diagonal constraints and aggregating them together before solving.
6/6
Examples and inspiration from: colab.research.google.com/github/philzoo…
and: ericpony.github.io/z3py-tutorial/…
h/t @SandMouth
</fin>
Share this Scrolly Tale with your friends.
A Scrolly Tale is a new way to read Twitter threads with a more visually immersive experience.
Discover more beautiful Scrolly Tales like this.