Assumptions & Logic: Supercharging SymPy

by Christian Muise for Python Software Foundation

In 2009, an assumption system (AS) was introduced to SymPy so users could reason about symbolic variables in a basic existential query. Underlying the AS, a logical boolean formula is constructed in CNF, and then solved by an internal SAT solver. At present, the system is limited in the types of queries it can perform -- mainly due to the efficiency of the underlying system. I propose to improve the reasoning engine in a number of ways that will significantly increase the efficiency of the AS.