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.

[Disha Holmukhe]

Hi Tilo,

Thank you for the detailed explanation! That makes complete sense. Creating extra clauses and making the SAT problem bigger definitely defeats the purpose of optimization. I am currently mapping out a preprocessing "simplification step" to catch and reject matrix/scalar predicates before the SAT solver is even invoked, exactly as you suggested. I will update #29162 with this approach soon.

In the meantime, I took your advice from the other day. I temporarily paused #29162 and looked for independent logic patches to help fulfill the GSoC requirement. Over the weekend, I submitted two new PRs touching core assumptions logic:

• PR #29555: Implemented the missing ZeroPredicate domain boundary logic for the inverse trig family (asin, atan, acos).

• PR #29557: Refactored the Pow assumptions handler to use clean, bidirectional Equivalent logic while protecting edge cases like 0^0=1.

Both are passing tests and are ready for review. If you or anyone else on the core team has a few spare minutes this week to take a look at either of them, I would be incredibly grateful, as I'm hoping to get one merged to fulfill the GSoC patch requirement.

(I have also officially submitted my final proposal to the GSoC portal and added it to the SymPy Wiki!)

Thanks again for all the incredible guidance this week.

Best,
Disha

To view this discussion visit https://groups.google.com/d/msgid/sympy/CAEgDm33MMkwDJqjdmHEP5FmZdVOw9tW-JiUz0jr6S4eu855v8g%40mail.gmail.com.