Now, the eighth week of official coding period has ended. I would give you a summary of my work during this week.
I spent most of this week polishing and finishing my work on #17144. The performance gain from this PR was very subtle but I had tested this only on the /assumptions/tests of SymPy. During this week’s meeting, Aaron suggested an example that had become slower than before:
1
2
p = random_poly(x, 10, -10, 10)
ask(Q.positive(p), Q.positive(x))
This made me realize that my strategy had a flaw. I had converted the smallest expressions into CNF objects and applied Boolean functions (or, and, and not) on them keeping the CNF structure intact. The performance regression was coming from operations or and not. In case of CNF structures, the number of expressions increased exponentially for these operations. Since the test suite didn’t have such examples, all the tests passed without any visible performance issue.
With some research, I found that the best approach to handle this (without any kind of pruning) was to convert these expression into NNF form first. So, I implemented a function to_NNF which works with low-level constructs (SymPy’s to_nnf would have been too costly) and converts an expression into NNF. This is then converted into CNF with ease. It keeps the number of clauses in check and hence also increases the performance outcome. The results are such: the above example now takes about 0.4 s on this PR while it takes about 6 s in master.
Currently, the work on this PR is almost complete and it is under review.
For the next week,
- My first priority is to get #17144 merged.
- Then, work on optimizing
rcall. This is an extension for the above work.
Will keep you updated. Thank you !