Week 0: The Start of GSoC

Created on May 24, 2026

2026   ·   sympy   python   ·   open-source

Starting with something new, a little excited as well as nervous with stuff. The incoming blogs will be me describing details of my project and stuff I did over the course of my period in GSoC’26 in SymPy.

Pre-GSoC

I have been contributing to SymPy for some time and was interested in contributing to the assumptions module. I had few merged PRs in the model (with a little different vision with respect to my project).

Mostly it involved me fixing bugs with recursive handlers in ask. A lot of it was also adding appropriate tests to counter various cases and check if the algorithm is working correctly. Soon, I had a talk with one of the collaborators Tilo, discussing various aspects I can make assumptions system better. The conversation. The discussion gave me a much clearer idea on what to work on over the summer and thus framing my proposal. Link to my proposal.

Results were announced on 30th April, I got in with 4 of my co-contributors and their projects under SymPy for 2026. I had my final exams for 4th semester were going on, so I did not start immediately. My mentors are Tilo and Aaron. I had my first meet on 18th May, 9:30 PM (Yeah a time which was suitable for both my mentors and me :D)

The Research Paper

The initial meet had us discussing what could be a good start for me to get going with the existing SAT Solvers in SymPy. One idea was to implement the backtracking function from the paper A Fast Linear-Arithmetic Solver for DPLL(T), this is the original paper on which the lra_solver has been developed. The backtracking function has been explained in the section 4.4 of the paper.

Let’s try to understand the research paper:

At a high level DPLL(T) separates the heavy lifting into two parts: a boolean SAT solver that handles the logical structure, and a Theory solver (Linear Real Arithmetic, or LRA) that checks if the current set of mathematical assertions is actually feasible.

The solver tracks three main things at all times:

  • The Tableau: A matrix that defines the relationships between variables. Variables are split into two camps: Basic (dependent) and Non-basic (independent).
  • The Bounds: Every variable has a lower and upper bound (initially $-\infty$ and $\infty$).
  • The Assignment ($\beta$): A mapping that gives every variable a specific numerical value to ensure the equations are always balanced.

Assert

When a constraint is fed into the solver, the Assert operation comes in. It doesn’t look in the matrix and doesn’t care about how variables are related.

It does a superficial check looking at the bounds of the specific variable. It updates the bound in $O(1)$ time and immediately checks for trivial contradictions.

For example - if the solver already knows $x \ge 5$, and we assert $x \le 2$, Assert flags the inconsistency instantly.

Check

Assert only looks at variable in isolation, it might end up passing systemic conflicts.

Check looks at the matrix to see if any basic variables violate their bounds. If a basic variable is out of bounds, Check attempts to fix it by pivoting meaning to swapping a basic variable with a non-basic variable to push the values back into a valid range.

If Check needs to adjust a variable but every single non-basic variable in that row is already maxed out at its own restrictive bound, the solver is trapped. It has mathematically proven that no valid assignment exists, and it raises a systemic conflict.

Backtrack

This is what I had to majorly focus on and implement. Let’s try to understand how it works.

When a conflict is raised, the solver has to back up. If it had to rebuild its entire matrix from scratch every time it hit a dead end, the solver would be impossibly slow.

Section 4.4 of the paper outlines an elegant solution: tracking the state history so that backtracking takes $O(1)$ time.

This is achieved using a state stack. Every time a bound is updated, the previous state is pushed onto the stack. When a conflict is detected, the solver simply pops the most recent update, restores the previous bound, and rolls back the variable assignments ($\beta$) to their last valid state snapshot.

Example

Section 4.6 (Figure 5) of the paper provides a specific sequence using two slack variables ($s_1$ and $s_2$):

  1. $x \le -4$
  2. $x \ge -8$
  3. $-x + y \le 1$ (which asserts $s_1 \le 1$)
  4. $x + y \ge -3$ (which asserts $s_2 \ge -3$)

The first three rules are asserted correctly. When rule 4 is fed into the system, Assert passes it completely fine because $s_2$ has no previous restrictive bounds.

But when Check runs, it is forced to pivot the matrix. During the pivot, it realizes that both $x$ and $s_1$ are maxed out, causing an inconsistency.

We backtrack after this failure and it proves the solver can safely unroll the matrix pivots in $O(1)$ complexity.

Implementation

The implementation will be done in the next week, following the next meet. Something to look forward to! :D

Sujal Kumar