If you care about optimization, use maths to simplify the problem before the search. Starting from the bottom.
(x / 1) mod 10 == 0
so you know the last digit is 0. This condition can then be discarded once you restrict generation to have the last digit as 0
.
This basically simplifies the problem to a nine-digit problem.
(x / 10) mod 9 == 0
Numbers are divisible by 9 if the sum of all the individual digits is evenly divisible by 9.
http://www.aaamath.com/div66_x9.htm
So this doesn't tell us anything (assuming it's true for any order, which it is), and we can drop the condition.
(x / 100) mod 8 == 0
This means x
can end in 0, 2, 4, 6, or 8. 0 is already used, so that only leaves 2, 4, 6 or 8.
x = ? ? ? ? ? ? ? even ? 0
where
even = [2, 4, 6, 8]
We can do the same for the even constraints
(x / 10000) mod 6 == 0
(x / 1000000) mod 4 == 0
(x / 100000000) mod 2 == 0
Giving
x = ? even ? even ? even ? even ? 0
where
even = [2, 4, 6, 8]
Thus the others are odd
x = odd even odd even odd even odd even odd 0
(x / 1000) mod 7 == 0
doesn't tell anything obvious yet, but keep it in mind.
(x / 10000) mod 6 == 0
tells us the value to that point is divisible by 3. Divisibility by 3 can be checked by saying the sum of its digits is congruent to 0 modulo 3.
x = odd even odd even odd even odd even odd 0
-------------------------- ------------
The second underlined group's sum of digits must thus be also divisible by 3 (as both groups together have a digit sum divisible by 3). We also know the value is odd.
x = odd even odd even odd even (genOddDiv3 ((d8 + d9) mod 3)) d8∈even d9∈odd 0
where
even = [2, 4, 6, 8]
odd = [1, 3, 5, 7, 9]
genOddDiv3 0 = [3, 9]
genOddDiv3 1 = [5]
genOddDiv3 2 = [1, 7]
(x / 100000) mod 5 == 0
tells us the digit is 5.
x = odd even odd even 5 even (genOddDiv3 ((d8 + d9) mod 3)) d8∈even d9∈odd 0
where
even = [2, 4, 6, 8]
odd = [1, 3, 7, 9]
genOddDiv3 0 = [3, 9]
genOddDiv3 1 = []
genOddDiv3 2 = [1, 7]
The lack of solutions for genOddDiv3
restricts d8
, but we can keep that in mind for later.
(x / 1000000) mod 4 == 0
tells us not all too much extra, but keep it in mind.
(x / 10000000) mod 3 == 0
tells us again that we have a divisibility constraint.
x = odd even odd even 5 even (genOddDiv3 ((d8 + d9) mod 3)) d8∈even d9∈odd 0
------------ -----------
where
even = [2, 4, 6, 8]
odd = [1, 3, 7, 9]
genOddDiv3 0 = [3, 9]
genOddDiv3 1 = []
genOddDiv3 2 = [1, 7]
Both underlined groups have a digit sum divisible by 3. This gives
x = (genOddDiv3 ((d2 + d3) mod 3)) d2∈even d3∈odd
(genEvenDiv3 ((5 + d6) mod 3)) 5 d6∈even
(genOddDiv3 ((d8 + d9) mod 3)) d8∈even d9∈odd
0
where
even = [2, 4, 6, 8]
odd = [1, 3, 7, 9]
genOddDiv3 0 = [3, 9]
genOddDiv3 1 = []
genOddDiv3 2 = [1, 7]
genEvenDiv3 0 = [6]
genEvenDiv3 1 = [4]
genEvenDiv3 2 = [2, 8]
The last two constraints again tell us nothing we didn't already know.
Which constraints haven't we entirely used?
(x / 100) mod 8 == 0
(x / 1000) mod 7 == 0
(x / 1000000) mod 4 == 0
Divisibility by 4 only depends on the last two values, so we can just list some things
00 04 08
12 16
20 24 28
32 36
40 44, 48
...
Namely, if the second digit is in [0, 4, 8], the first is even. If the second digit is in [2, 6], the first is odd. Since the first (d3
) is odd, we know the second must be in [2, 6].
x = (genOddDiv3 ((d2 + d3) mod 3)) d2∈even d3∈odd
(genD4 ((5 + d6) mod 3)) 5 d6∈even
(genOddDiv3 ((d8 + d9) mod 3)) d8∈even d9∈odd
0
where
even = [2, 4, 6, 8]
odd = [1, 3, 7, 9]
genOddDiv3 0 = [3, 9]
genOddDiv3 1 = []
genOddDiv3 2 = [1, 7]
genD4 0 = [6]
genD4 1 = []
genD4 2 = [2]
The same can be done for (x / 100) mod 8 == 0
, which implies (x / 100) mod 4 == 0
.
x = (genOddDiv3 ((d2 + d3) mod 3)) d2∈even d3∈odd
(genD4 ((5 + d6) mod 3)) 5 d6∈even
(genOddDiv3 ((d8 + d9) mod 3)) d8∈[2, 6] d9∈odd
0
where
even = [2, 4, 6, 8]
odd = [1, 3, 7, 9]
genOddDiv3 0 = [3, 9]
genOddDiv3 1 = []
genOddDiv3 2 = [1, 7]
genD4 0 = [6]
genD4 1 = []
genD4 2 = [2]
We can use genOddDiv3 1 = []
to filter d8
dependent on d9
, and the fact both d8
and d4
are in [2, 6]
to filter d2
and d6
to [4, 8]
. We can do the same filtering on d2
too.
x = (genOddDiv3 ((d2 + d3) mod 3)) d2∈[4, 8] d3∈odd
(genD4 ((5 + d6) mod 3)) 5 d6∈[4, 8]
(genOddDiv3 ((d8 + d9) mod 3)) d8∈(genD8 d9) d9∈odd
0
where
odd = [1, 3, 7, 9]
genOddDiv3 0 = [3, 9]
genOddDiv3 1 = []
genOddDiv3 2 = [1, 7]
genD8 1 = [2]
genD8 3 = [2, 6]
genD8 7 = [2]
genD8 9 = [2, 6]
genD4 0 = [6]
genD4 1 = []
genD4 2 = [2]
genD2 1 = [4, 8]
genD2 3 = [8]
genD2 7 = [4, 8]
genD2 9 = [8]
Then we can use specialize D4
on d6
's possibilities, which shows us d6 = 4
, d4 = 6
. Thus d8 = 2
and d2 = 8
.
x = (genOddDiv3 ((8 + d3) mod 3)) 8 d3∈odd
6 5 4
(genOddDiv3 ((2 + d9) mod 3)) 2 d9∈odd
0
where
odd = [1, 3, 7, 9]
genOddDiv3 0 = [3, 9]
genOddDiv3 1 = []
genOddDiv3 2 = [1, 7]
Then specialize the genOddDiv3
s on their input.
x = (genD1 d3) 8 d3∈odd
6 5 4
(genD7 d9 ((2 + d9) mod 3)) 2 d9∈odd
0
where
odd = [1, 3, 7, 9]
genD1 1 = [3, 9]
genD1 3 = [1, 7]
genD1 7 = [3, 9]
genD1 9 = [1, 7]
genD9 = genD1
Our options are now easily enumerable:
x = 1836547290
x = 3816549270
x = 3876549210
x = 7836541290
x = 7896541230
x = 7896541230
x = 9816543270
x = 9876543210
and we can test each for divisibility by 7
183654 mod 7 = 2
381654 mod 7 = 0
387654 mod 7 = 1
783654 mod 7 = 4
789654 mod 7 = 5
789654 mod 7 = 5
981654 mod 7 = 2
987654 mod 7 = 3
So our only solution is
381654
Ergo the most efficient Haskell I can think of is
pizza = 3816549270