Skip to main content
Code Review

Return to Answer

deleted 216 characters in body
Source Link
Veedrac
  • 9.8k
  • 23
  • 38
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]
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]
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]
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]
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]
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
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]
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]
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]
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]
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]
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
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]
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]
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]
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]
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]
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
Source Link
Veedrac
  • 9.8k
  • 23
  • 38

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 genOddDiv3s 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
lang-hs

AltStyle によって変換されたページ (->オリジナル) /