Three Simple Math Problems
April 12, 2019
You can watch the videos to see the analytical solutions. Here are programming solutions to the three problems:
> (do ((y 10 (+ y 1))) ((square? (- (expt 2 y) 615)) (list (isqrt (- (expt 2 y) 615)) y))) (59 12)
> (list-of (list a b c) (a range 1 10) (b range 1 10) (c range 1 10) (= (+ (* 100 a) (* 10 b) c) (+ (fact 1) (fact b) (fact c)))) ((1 4 5))
> (list-of (list p i e) (p range 1 10) (i range 1 10) (e range 1 10) (= (+ (sqrt (+ (* 10 p) i)) e) (sqrt (+ (* 100 p) (* 10 i) e)))) ((1 6 9))
You can run the program at https://ideone.com/DEm8X7.
Here’s a Haskell solution. I decided that overkill was appropriate and used the Z3 SMT solver via the SBV library. Problem 3 turned out to the most difficult one, as the straightforward problem statement mixed integers and algebraic reals which current solvers have great difficulty with. Reorganizing the expression to use only integers fixed that issue. (Also, the factorial function had to be written in a particular way to prevent the solver from going off the rails…)
{-# LANGUAGE ScopedTypeVariables #-} import Data.SBV prob1 = optimize Lexicographic $ do [x, y] <- sWord32s ["x", "y"] constrain $ 615 + x*x .== 2.^y minimize "min |x|" $ abs x minimize "min y" y prob2 = sat $ do [a, b, c] <- sWord32s ["a", "b", "c"] solve [ a .> 0 &&& a .< 10 , b .> 0 &&& b .< 10 , c .> 0 &&& c .< 10 , 100*a + 10*b + c .== fact' a + fact' b + fact' c ] where fact' = fact 10 fact :: SWord32 -> SWord32 -> SWord32 fact top n = fact1 1 1 where fact1 prev m = ite (m .== top ||| m .== n) (m * prev) (fact1 (m * prev) (m + 1)) prob3 = sat $ do [p, i, e] <- sIntegers ["p", "i", "e"] let pie = 100*p + 10*i + e pi = 10*p + i solve [ p .> 0 &&& p .< 10 , i .> 0 &&& i .< 10 , e .> 0 &&& e .< 10 -- sqrt (pi) + e .== sqrt (pie) => , pi .== ((pie - pi - e^2) `sDiv` (2*e))^2 ]