GSoC 2026 Proposal Draft: Refactoring Fact Extraction & SAT Solver Optimization

[Disha Holmukhe]

Hi everyone,

I'm Disha (Kiwi-520), a final-year IT Engineering student. Over the last few months, I've really enjoyed contributing to SymPy (with recent merged PRs #29009, #28889, and #28761).

While recently working on PR #29162 (adding Matrix/Scalar boundary logic to the SAT registry), I've been looking deeper into the extraction blindspots in satask.py that cause the solver to bypass the sathandlers registry during complex nested queries.

I am putting together my GSoC proposal to tackle this. My goal is to build a recursive AST extraction pipeline to prevent nested variables from being missed, expand the sathandlers registry for advanced mathematical boundaries, and implement a lazy-evaluation staging layer to catch local contradictions before the expensive CNF conversion takes place.

I've put together a draft of my proposal with a 12-week timeline mapping out these three phases. I would love to get your feedback on the scope and technical direction before final submission!

Link to my proposal draft: Proposal

Thanks so much for your time and guidance!

Best, 
Disha
Github

[Tilo RC]

Hi Disha, 

It doesn't look like you've satisfied the patch requirement yet. If your open pull request got merged 

that would probably be enough to satisfy the requirement, but the approach it uses is not ideal 

so in its current form it's unlikely to get merged. Your existing merged pull requests look like they 

improve documentation and add tests which is not enough to satisfy the requirement. 

I'm not sure what the official SymPy policy is, but you probably have a bit of extra time after you

submit your proposal to Google to get a pull request that fulfills the patch requirement merged. 

The process of fulfilling the patch requirement can take a lot of time because it might take a while

for people to get around to reviewing a pull request and it might not become clear that a certain approach 

is wrong until after putting a lot of work into it. 

So if you want to have a proposal that doesn't automatically get disqualified, you might want to try to 

opening new pull requests that might get finished sooner as I'm not sure how long it would take for your 

current PR to be finished. 

Sincerely, 

Tilo

[Disha Holmukhe]

Hi Tilo,

Thank you so much. I really appreciate you looking out for my proposal and taking the time to review my PR history.

I completely understand the policy regarding the patch requirement needing to be a core logic/code change rather than just tests or documentation. It makes total sense.

Regarding my open PR (#29162), I would love to learn why the current approach isn't ideal when you have a spare moment. Understanding the architectural flaw in my approach will definitely help me write better code for SymPy going forward.

In the meantime, I am taking your advice immediately. I am going to pause work on #29162 and look for a smaller, independent logic bug to fix so I can get a qualifying patch merged as soon as possible.

Thanks again for the guidance.

Best, Disha

--
You received this message because you are subscribed to the Google Groups "sympy" group.
To unsubscribe from this group and stop receiving emails from it, send an email to sympy+un...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/sympy/5b04cebb-d55e-42dd-9963-b8756b4991c1n%40googlegroups.com.

[Tilo RC]

Hi Disha,

>  I would love to learn why the current approach isn't ideal

I left this comment in the PR:

> It would be more computationally efficient to do a simplification step before the sat solver is involved.

> This is going to add extra clauses which will make the overall clause structure bigger and slow things down.

To elaborate, your PR add facts that tells the sat solver that scalar predicates applied to matrices should be false.

This approach is going to be slower than replacing such predicates applied to matrices in a preprocessing step since

creating the extra clauses is expensive and solving a bigger sat problem is also more expensive. 

Sincerely,

Tilo RC

You received this message because you are subscribed to a topic in the Google Groups "sympy" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/sympy/46nCyzdteVk/unsubscribe.
To unsubscribe from this group and all its topics, send an email to sympy+un...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/sympy/CAEM2JmfEO1HktfUP%3D0B%3DrwYb17SqjPPMuKAsxdF%3DmbnmR6avsg%40mail.gmail.com.