A Sentient program to find solutions to questions posed in 'Digit Reversal Without Apology'

digit-reversal.snt

#!/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]}
# {}