Last active
October 27, 2019 00:14
-
-
Save tuzz/f9cfe0ea21f694c40158c1a783de3d31 to your computer and use it in GitHub Desktop.
A Sentient program to find solutions to questions posed in 'Digit Reversal Without Apology'
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/usr/bin/env sentient -c -o -r -n 0 -m lingeling digit-reversal.snt | |
# https://arxiv.org/pdf/math/0511366.pdf | |
# This program explores 'Open question one' | |
array5<int9> digits; | |
base = 198; | |
max = 197; | |
digits.each(function^ (d) { invariant d.between?(0, max); }); | |
decimal1 = digits.reduce(0, function^ (sum, d) { return sum * base + d; }); | |
decimal2 = digits.reverse.reduce(0, function^ (sum, d) { return sum * base + d; }); | |
int9 k; | |
invariant k.between?(2, max); | |
invariant k * decimal1 == decimal2; | |
invariant digits[0] != 0; | |
invariant digits[4] != 0; | |
expose digits, k; | |
array4<int9> smaller; | |
invariant smaller[0] == digits[0]; | |
invariant smaller[1] == digits[1]; | |
invariant smaller[2] == digits[3]; | |
invariant smaller[3] == digits[4]; | |
smaller.each(function^ (d) { invariant d.between?(0, max); }); | |
decimal3 = smaller.reduce(0, function^ (sum, d) { return sum * base + d; }); | |
decimal4 = smaller.reverse.reduce(0, function^ (sum, d) { return sum * base + d; }); | |
# max | |
2.upto(197, function^ (k2) { | |
invariant k2 * decimal3 != decimal4; | |
}); | |
fp = digits[0] - digits[1] + digits[2] - digits[3] + digits[4]; | |
invariant fp != 0; | |
expose fp; | |
# Testing with base=30, max=29: (the fp != 0 was removed for testing) | |
# {"k":3,"f":0,"digits":[3,22,15,7,11]} | |
# {"k":8,"f":0,"digits":[2,13,8,16,19]} <-- There's a mistake in the paper, 9 should be 19. | |
# {} | |
# | |
# Solutions for base 40: <-- I think the following solutions answer question one. | |
# {"k":13,"fp":41,"digits":[2,24,30,1,34]} | |
# {} | |
# | |
# Solutions for base 46: | |
# {"k":25,"fp":47,"digits":[1,18,40,11,35]} | |
# {"k":13,"fp":47,"digits":[2,21,42,8,32]} | |
# {} | |
# | |
# Solutions for base 52: | |
# {"k":22,"fp":53,"digits":[2,3,39,30,45]} | |
# {} | |
# | |
# Solutions for base 82: | |
# {"k":34,"fp":83,"digits":[2,5,37,21,70]} | |
# {} | |
# | |
# Solutions for base 166: | |
# {"k":49,"fp":167,"digits":[1,40,159,14,61]} | |
# {} | |
# | |
# Solutions for base 172: | |
# {"k":77,"fp":173,"digits":[1,62,156,27,105]} | |
# {} | |
# | |
# Solutions for base 178: | |
# {"k":16,"fp":179,"digits":[4,34,166,24,67]} | |
# {} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment