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

add readme

Browse Source
This commit is contained in:
Florian Stecker 2024-08-28 15:43:07 -04:00
parent 74ffaea4c0
commit d0757e3471
1 changed files with 57 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

57
README.md Normal file
View File

@ -0,0 +1,57 @@
# Symbolic solver for polynomials with rational coefficients #
## Program output ##
Equation: (x + 50) * 10 - 150 = 100
Parsed: (- (- (* (+ x 50) 10) 150) 100)
Factorized normal form: 10(25 + 1x)
Solutions: { x = -25 }
Equation: (x - 2) * (x + 2) = 0
Parsed: (- (* (- x 2) (+ x 2)) 0)
Factorized normal form: (-2 + 1x)(2 + 1x)
Solutions: { x = 2, x = -2 }
Equation: x ^ 2 = 4
Parsed: (- (^ x 2) 4)
Factorized normal form: (-4 + 0x + 1x^2)
Solutions: { x = 2, x = -2 }
Equation: x ^ 2 - 2 = 0
Parsed: (- (- (^ x 2) 2) 0)
Factorized normal form: (-2 + 0x + 1x^2)
Solutions: { x = 2 ^ (1/2), x = -2 ^ (1/2) }
Equation: x ^ 2 = 2 * x + 15
Parsed: (- (^ x 2) (+ (* 2 x) 15))
Factorized normal form: (-15 + -2x + 1x^2)
Solutions: { x = 5, x = -3 }
Equation: (x ^ 2 - 2 * x - 15) * (x + 5) = 0
Parsed: (- (* (- (- (^ x 2) (* 2 x)) 15) (+ x 5)) 0)
Factorized normal form: (-15 + -2x + 1x^2)(5 + 1x)
Solutions: { x = 5, x = -3, x = -5 }
Equation: x ^ 3 + 3 * x ^ 2 - 25 * x - 75 = 0
Parsed: (- (- (- (+ (^ x 3) (* 3 (^ x 2))) (* 25 x)) 75) 0)
Factorized normal form: (3 + 1x)(-25 + 0x + 1x^2)
Solutions: { x = -3, x = 5, x = -5 }
Equation: x ^ 3 - 91 * x - 90 = 0
Parsed: (- (- (- (^ x 3) (* 91 x)) 90) 0)
Factorized normal form: (-90 + -91x + 0x^2 + 1x^3)
Guessing rational solutions: 10, -9, -1
Verified guessed solutions!
Solutions: { x = 10, x = -9, x = -1 }
## Notes ##
This uses an egraph with rewrite rules representing the usual rules of arithmetic, and constant folding with rational numbers. This alone is enough to solve linear equations, by just starting with the difference of the two sides and minimizing AST size. However, it can't suffice for quadratic equations, as the egraph can't create values "out of this air". For example, to solve `x^2 = 2` the egraph must at least have "seen" the expression `2^(1/2)` once.
So instead, I used the egraph to bring the expression into a standard form: a product of monic polynomials in standard form, where the product is supposed to be factored out as much as possible. Since this is difficult to model with a cost function, I wrote a custom extractor which tries to recover an expression of this form from the egraph.
Then we can use the usual quadratic formula to find solutions. The obtained solutions are 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.
Finally, the unfactorized cubic equation from the examples gets factored into a linear and a quadratic factor by the egraph. This is kind of "magic" though, and for general cubics (even if they have integer solutions) we can't expect that to happen (see the additional last example). So I used another strategy to deal with cubic equations with rational solutions: they are solved numerically, the numerical solutions are approximated by rational numbers using continued fractions, and then the result is verified by using an egraph to see if the factization is equivalent to the original polynomial.
Finally, this has essentially only been tested on the 8 examples above. So I would expect there to still be a few bugs.