Symbolic solver for polynomials with rational coefficients

Program output

Using cargo run --release. On my laptop, the last example times out on debug settings.

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, the egraph is used to bring the expression into a standard form: a product of monic polynomials which is factored as much as possible. Since this is difficult to model with a cost function, I wrote a custom extractor (in normal_form.rs).

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 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.