florian/solveq
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

slightly clarify the explanation

Browse Source
This commit is contained in:
Florian Stecker 2024-08-29 09:31:44 -04:00
parent 829f1e7fa7
commit fced3915ea
1 changed files with 3 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
README.md
View File

@ -54,6 +54,8 @@ So instead, the egraph is used to bring the expression into a standard form: a p
Then we can use the usual quadratic formula to find solutions. The obtained solutions are afterwards simplified by another egraph, with a special "square root of a square integer" rule. This is pretty minimal, a more complete solution would also be able to deal with square roots of rational numbers etc. Then we can use the usual quadratic formula to find solutions. The obtained solutions are afterwards simplified by another egraph, with a special "square root of a square integer" rule. This is pretty minimal, a more complete solution would also be able to deal with square roots of rational numbers etc.
Finally, the unfactorized cubic equation (equation 7) gets factored into a linear and a quadratic factor by the egraph. This is kind of "magic" though (the right factor just seems to randomly come up elsewhere), and for general cubics we can't expect that to happen, even if they have integer solutions. The additional equation 8 is an example for this. So we use another strategy to deal with cubic equations with rational solutions: we solve the equation numerically using the general cubic formula, then approximate the numerical solutions by rational numbers using continued fractions. Finally, we verify the result by using an egraph to see if the obtained factorization is equivalent to the original polynomial. This equivalence check required increased node and iteration limits, and takes a few seconds on my laptop. Finally, the unfactorized cubic equation (equation 7) gets factored into a linear and a quadratic factor by the egraph. This is kind of "magic" though: the correct terms seem to come up randomly while mutating the egraph. For general cubics we can't expect this to happen, even if they have integer solutions. The additional equation 8 is an example for this.
While there is a general formula for the solutions of a cubic equation, it contains trigonometric functions and/or complex numbers, and we don't want to deal with that here. So we use a different strategy which can handle cubic equations with 3 rational solutions: we first solve the equation numerically using the cubic formula, then find rational expressions for the numerical solutions using continued fractions. Finally, we verify the resulting factorization by using an egraph. This equivalence check required increased node and iteration limits, and takes a few seconds on my laptop.
This has essentially only been tested on the 8 examples above. So I would expect there to still be a few bugs. The algorithm is also spectacularly inefficient, considering that the equality of rational polynomials is almost trivial to compute. This has essentially only been tested on the 8 examples above. So I would expect there to still be a few bugs. The algorithm is also spectacularly inefficient, considering that the equality of rational polynomials is almost trivial to compute.