THIS IS A DRAFT OF AN UPCOMING BLOG POST. IT’S ALMOST FINISHED BUT STILL INCOMPLETE. If you’re not familiar with what SymPy’s assumptions are, read about the old assumptions and new assumptions he...

Are you tired of crawling the web for good tutorials for writing your own SMT solver? Is everything you find is either a 300 slide long powerpoint presentation or a dense paper? Well you’re in luc...

I’ll be walking through some examples of problems SAT and SMT solvers solve. Then I’ll be using python wrappers for PicoSAT and Z3 to solve the example problems. If you’re familiar with python, you...

Hello! Welcome to the first weekly update on my Google Summer of Code project with SymPy. SymPy is an open-source Python library for symbolic computation: think WolframAlpha but a Python library. ...