Search for polynomial roots

Question

Given a polynomial of degree n, how can I reliably find all the values ​​of x, where y = 0.

I am currently using a library Math.Polynomialthat does not seem to be built into this function. something is missing here, it looks like it will be a widely used function.

thank

Answer 1

You can use the Polynomial.Rootspackage module dsp. It deals with complex values ​​(complex coefficients and complex roots).

For example, to solve 1+2x+2x²=0:

Prelude> import Polynomial.Roots 
Prelude Polynomial.Roots> roots 1e-16 1000 [1,2,2]
[(-0.5) :+ (-0.5),(-0.5) :+ 0.5]

As a health check, R gives the same result:

> polyroot(c(1,2,2))
[1] -0.5+0.5i -0.5-0.5i

Answer 2

If you don't mind using an external SMT solver, you can use the SBV package:

Prelude Data.SBV> allSat $ \x -> 2*x^3-19*x^2+15*x+72 .== (0::SReal)
Solution #1:
  s0 = 3.0 :: Real
Solution #2:
  s0 = 8.0 :: Real
Solution #3:
  s0 = -1.5 :: Real
Found 3 different solutions.

, , .. . Real . , :

Prelude Data.SBV> allSat $ \x -> x^2-2 .== (0::SReal)
Solution #1:
  s0 = root(1, x^2 = 2) = -1.414213562373095... :: Real
Solution #2:
  s0 = root(2, x^2 = 2) = 1.414213562373095... :: Real
Found 2 different solutions.

:

Prelude Data.SBV> allSatWith z3{printRealPrec=20} $ \x -> x^2-2 .== (0::SReal)
Solution #1:
  s0 = root(1, x^2 = 2) = -1.4142135623730950488... :: Real
Solution #2:
  s0 = root(2, x^2 = 2) = 1.4142135623730950488... :: Real
Found 2 different solutions.

, SMT ; :

Prelude Data.SBV> allSat $ \x -> x^2+1 .== (0::SReal)
No solutions found.

, :

Prelude Data.SBV> allSat $ \x -> x^3+2*x-1 .== (0::SReal)
Solution #1:
  s0 = root(1, x^3+2x = 1) = 0.4533976515164037... :: Real
This is the only solution.

PS. , Z3 . https://github.com/Z3Prover/z3/releases