""" Shifted division in Picat. https://twitter.com/queued_q/status/1315505135246663682 ''' 7903225806451612 7 ----------------- = - 9032258064516128 8 ''' This is represented as x/y = a/b Note that a (here 7) is the first digit of x and b (here 8) is the last digit of y. These constraints are what make it interesting problem. * Speed The approach here is simpler - and much faster - than shifted_division.py Finding all solutions for n=2..100 (i.e. the number of digits) takes 49.9s Here's a sample: n: 23 71014492753623188405797/10144927536231884057971 = 7/1 pattern: len:0 54347826086956521739130/43478260869565217391304 = 5/4 pattern: len:0 74242424242424242424242/42424242424242424242424 = 7/4 pattern:4242424242 len:10 39130434782608695652173/91304347826086956521737 = 3/7 pattern: len:0 n: 73 1428571428571428571428571428571428571428571428571428571428571428571428571/4285714285714285714285714285714285714285714285714285714285714285714285713 = 1/3 pattern:142857142857142857142857142857142857 len:36 1666666666666666666666666666666666666666666666666666666666666666666666666/6666666666666666666666666666666666666666666666666666666666666666666666664 = 1/4 pattern:666666666666666666666666666666666666 len:36 3461538461538461538461538461538461538461538461538461538461538461538461538/4615384615384615384615384615384615384615384615384615384615384615384615384 = 3/4 pattern:461538461538461538461538461538461538 len:36 7424242424242424242424242424242424242424242424242424242424242424242424242/4242424242424242424242424242424242424242424242424242424242424242424242424 = 7/4 Finding all 23 solutions of 1231 digit numbers takes 2min43.20s. Here is the first solution: 9759036144578313253012048192771084337349397590361445783132530120481927710843373493975903614457831325301204819277108433734939759036144578313253012048192771084337349397590361445783132530120481927710843373493975903614457831325301204819277108433734939759036144578313253012048192771084337349397590361445783132530120481927710843373493975903614457831325301204819277108433734939759036144578313253012048192771084337349397590361445783132530120481927710843373493975903614457831325301204819277108433734939759036144578313253012048192771084337349397590361445783132530120481927710843373493975903614457831325301204819277108433734939759036144578313253012048192771084337349397590361445783132530120481927710843373493975903614457831325301204819277108433734939759036144578313253012048192771084337349397590361445783132530120481927710843373493975903614457831325301204819277108433734939759036144578313253012048192771084337349397590361445783132530120481927710843373493975903614457831325301204819277108433734939759036144578313253012048192771084337349397590361445783132530120481927710843373493975903614457831325301204819277108433734939759036144578313253012048192771084337349397590361445783132530120481927710843373493975903614457831325301204819277108433734939/7590361445783132530120481927710843373493975903614457831325301204819277108433734939759036144578313253012048192771084337349397590361445783132530120481927710843373493975903614457831325301204819277108433734939759036144578313253012048192771084337349397590361445783132530120481927710843373493975903614457831325301204819277108433734939759036144578313253012048192771084337349397590361445783132530120481927710843373493975903614457831325301204819277108433734939759036144578313253012048192771084337349397590361445783132530120481927710843373493975903614457831325301204819277108433734939759036144578313253012048192771084337349397590361445783132530120481927710843373493975903614457831325301204819277108433734939759036144578313253012048192771084337349397590361445783132530120481927710843373493975903614457831325301204819277108433734939759036144578313253012048192771084337349397590361445783132530120481927710843373493975903614457831325301204819277108433734939759036144578313253012048192771084337349397590361445783132530120481927710843373493975903614457831325301204819277108433734939759036144578313253012048192771084337349397590361445783132530120481927710843373493975903614457831325301204819277108433734939759036144578313253012048192771084337349397 = 9/7 It has a repeated pattern (see below) of length 615: 975903614457831325301204819277108433734939759036144578313253012048192771084337349397590361445783132530120481927710843373493975903614457831325301204819277108433734939759036144578313253012048192771084337349397590361445783132530120481927710843373493975903614457831325301204819277108433734939759036144578313253012048192771084337349397590361445783132530120481927710843373493975903614457831325301204819277108433734939759036144578313253012048192771084337349397590361445783132530120481927710843373493975903614457831325301204819277108433734939759036144578313253012048192771084337349397590361445783132530120481927710843373493 * Interestingness/repeatability A shifted division x/y = a/b is 'interesting' if the x part is without any repeating pattern (see the method find_repeating_pattern). I first thought that this interestingness was more common when n (the number of digits) was a prime, but that conjecture is not true. Here are the interesting (non-repeating) divisions from n=2..100. The format is [n,x,y,a,b,is_prime] [6, 987804, 878048, 9, 8, False] [7, 7538461, 5384615, 7, 5, True] [7, 5952380, 9523808, 5, 8, True] [7, 3461538, 4615384, 3, 4, True] [7, 1428571, 4285713, 1, 3, True] [7, 4571428, 5714285, 4, 5, True] [7, 4102564, 1025641, 4, 1, True] [7, 8311688, 3116883, 8, 3, True] [7, 6428571, 4285714, 6, 4, True] [7, 2857142, 8571426, 2, 6, True] [7, 8205128, 2051282, 8, 2, True] [7, 6923076, 9230768, 6, 8, True] [9, 876712328, 767123287, 8, 7, False] [14, 67924528301886, 79245283018867, 6, 7, False] [14, 81012658227848, 10126582278481, 8, 1, False] [16, 7903225806451612, 9032258064516128, 7, 8, False] [17, 47058823529411764, 70588235294117646, 4, 6, True] [17, 23529411764705882, 35294117647058823, 2, 3, True] [17, 95294117647058823, 52941176470588235, 9, 5, True] [19, 4210526315789473684, 2105263157894736842, 4, 2, True] [19, 6315789473684210526, 3157894736842105263, 6, 3, True] [19, 8421052631578947368, 4210526315789473684, 8, 4, True] [19, 2105263157894736842, 1052631578947368421, 2, 1, True] [22, 5813953488372093023255, 8139534883720930232557, 5, 7, False] [22, 9418604651162790697674, 4186046511627906976744, 9, 4, False] [23, 71014492753623188405797, 10144927536231884057971, 7, 1, True] [23, 54347826086956521739130, 43478260869565217391304, 5, 4, True] [23, 39130434782608695652173, 91304347826086956521737, 3, 7, True] [29, 31034482758620689655172413793, 10344827586206896551724137931, 3, 1, True] [29, 93103448275862068965517241379, 31034482758620689655172413793, 9, 3, True] [29, 62068965517241379310344827586, 20689655172413793103448275862, 6, 2, True] [34, 7313432835820895522388059701492537, 3134328358208955223880597014925373, 7, 3, False] [42, 975903614457831325301204819277108433734939, 759036144578313253012048192771084337349397, 9, 7, False] [43, 5102040816326530612244897959183673469387755, 1020408163265306122448979591836734693877551, 5, 1, True] [45, 910112359550561797752808988764044943820224719, 101123595505617977528089887640449438202247191, 9, 1, False] [47, 53191489361702127659574468085106382978723404255, 31914893617021276595744680851063829787234042553, 5, 3, True] [59, 61016949152542372881355932203389830508474576271186440677966, 10169491525423728813559322033898305084745762711864406779661, 6, 1, True] Here is a solution for n=97 that looks quite interesting but is not (according to the above definition): 8767123287671232876712328767123287671232876712328767123287671232876712328767123287671232876712328/7671232876712328767123287671232876712328767123287671232876712328767123287671232876712328767123287 = 8/7 The pattern is 876712328767123287671232876712328767123287671232 and is of length 48 Why is there no interesting divisions between 60 and 100? What I can see, these 37 interesting divisions shown above are the first representations of the a/b divisions. Here is a sorted list of the values of (a,b,n) for each interesting divsion (what I call ratio numbers). ratio numbers (len: 37) (1, 3, 7) (2, 1, 19) (2, 3, 17) (2, 6, 7) (3, 1, 29) (3, 4, 7) (3, 7, 23) (4, 1, 7) (4, 2, 19) (4, 5, 7) (4, 6, 17) (5, 1, 43) (5, 3, 47) (5, 4, 23) (5, 7, 22) (5, 8, 7) (6, 1, 59) (6, 2, 29) (6, 3, 19) (6, 4, 7) (6, 7, 14) (6, 8, 7) (7, 1, 23) (7, 3, 34) (7, 5, 7) (7, 8, 16) (8, 1, 14) (8, 2, 7) (8, 3, 7) (8, 4, 19) (8, 7, 9) (9, 1, 45) (9, 3, 29) (9, 4, 22) (9, 5, 17) (9, 7, 42) (9, 8, 6) The reason for the few interesting divisions is that if there a previous (interesting) division with x/y = a/b, the divisions after that with the same ratio number a/b will then have an repeated x as a pattern, thus makes that division uninteresting. Example: Here is an interesting division for n=9 (the first for 8/7) 876712328/767123287 = 8/7 After that, all the other divisions with a/b = 8/7 will repeat 876712328 (x) as the pattern in some duplicity. Here are a few of these: n 17 87671232876712328/76712328767123287 = 8/7 pattern:87671232 len:8 n 25 8767123287671232876712328/7671232876712328767123287 = 8/7 pattern:87671232 len:8 n 33 876712328767123287671232876712328/767123287671232876712328767123287 = 8/7 pattern:8767123287671232 len:16 n 41 87671232876712328767123287671232876712328/76712328767123287671232876712328767123287 = 8/7 pattern:8767123287671232 len:16 n 49 8767123287671232876712328767123287671232876712328/7671232876712328767123287671232876712328767123287 = 8/7 pattern:876712328767123287671232 len:24 etc... Another note: There are 72 possible ratio numbers (A in 1..9, B in 1..9 and A != B). Some of the 72 possible ratio numbers are not in this list, for example 7/2. Why is there no 7/2? Is it not an interesting division? It's worse than that, for n=2..100 there is no 7/2 division at all. Why? It's the same thing for other divisions, e.g. 8/5. * Number of solutions Note that we remove solutions when x and y are identical since these are not really interesting at all. Here are the number of solutions for n=2..100 2 num_solutions: 4 True 3 num_solutions: 7 True 4 num_solutions: 6 False 5 num_solutions: 7 True 6 num_solutions: 5 False 7 num_solutions:20 True 8 num_solutions: 4 False 9 num_solutions: 8 False 10 num_solutions: 6 False 11 num_solutions: 8 True 12 num_solutions: 4 False 13 num_solutions:20 True 14 num_solutions: 6 False 15 num_solutions: 7 False 16 num_solutions: 8 False 17 num_solutions:11 True 18 num_solutions: 4 False 19 num_solutions:24 True 20 num_solutions: 4 False 21 num_solutions: 8 False 22 num_solutions: 8 False 23 num_solutions:10 True 24 num_solutions: 4 False 25 num_solutions:21 False 26 num_solutions: 5 False 27 num_solutions: 9 False 28 num_solutions: 6 False 29 num_solutions:10 True 30 num_solutions: 4 False 31 num_solutions:22 True 32 num_solutions: 4 False 33 num_solutions:11 False 34 num_solutions: 7 False 35 num_solutions: 7 False 36 num_solutions: 5 False 37 num_solutions:24 True 38 num_solutions: 4 False 39 num_solutions: 7 False 40 num_solutions: 8 False 41 num_solutions: 9 True 42 num_solutions: 5 False 43 num_solutions:23 True 44 num_solutions: 4 False 45 num_solutions:11 False 46 num_solutions: 8 False 47 num_solutions: 8 True 48 num_solutions: 4 False 49 num_solutions:24 False 50 num_solutions: 4 False 51 num_solutions: 8 False 52 num_solutions: 6 False 53 num_solutions: 9 True 54 num_solutions: 4 False 55 num_solutions:24 False 56 num_solutions: 5 False 57 num_solutions:11 False 58 num_solutions: 6 False 59 num_solutions: 8 True 60 num_solutions: 4 False 61 num_solutions:22 True 62 num_solutions: 4 False 63 num_solutions: 7 False 64 num_solutions: 8 False 65 num_solutions:11 False 66 num_solutions: 7 False 67 num_solutions:24 True 68 num_solutions: 4 False 69 num_solutions: 7 False 70 num_solutions: 6 False 71 num_solutions: 8 True 72 num_solutions: 4 False 73 num_solutions:25 True 74 num_solutions: 4 False 75 num_solutions: 7 False 76 num_solutions: 8 False 77 num_solutions: 7 False 78 num_solutions: 4 False 79 num_solutions:22 True 80 num_solutions: 4 False 81 num_solutions:12 False 82 num_solutions: 6 False 83 num_solutions: 8 True 84 num_solutions: 4 False 85 num_solutions:26 False 86 num_solutions: 5 False 87 num_solutions: 7 False 88 num_solutions: 6 False 89 num_solutions:12 True 90 num_solutions: 4 False 91 num_solutions:26 False 92 num_solutions: 6 False 93 num_solutions: 8 False 94 num_solutions: 6 False 95 num_solutions: 7 False 96 num_solutions: 5 False 97 num_solutions:24 True 98 num_solutions: 4 False 99 num_solutions: 7 False 100 num_solutions: 7 False It seems that when n is a prime there are more solutions than for (most( composite numbers. However, I cannot not see the direct pattern in this sequence. Testing in OEIS (https://oeis.org/) give no solution: 4, 7, 6, 7, 5, 20, 4, 8, 6, 8, 4, 20, 6, 7, 8, 11, 4,24 This Z3 model was written by Hakan Kjellerstrand (hakank@gmail.com) See also my Z3 page: http://hakank.org/z3/ """ from z3 import * import time, re def find_repeating_pattern(s): """ find_repeating_pattern(s) For the division x/y = a/b try to find a repeating pattern in x. We require at least a pattern of 2 digits, thus the length of the string must be at least 5 digits (ignoring the first digit). """ m = re.search(r"(\d{2,})\1",s) if m == None: return "" else: return m.group(1) def is_prime(num): """ Is num a prime? """ if num < 2: return False if not num & 1: return num == 2 div = 3 while div * div <= num: if num % div == 0: return False div += 2 return True non_repeating = [] # Which solutions are non repeating (interesting)? ratio_numbers = [] # What n "covers" a specific ratio? def shifted_division2(n): t0 = time.time() min_val = 10**(n-1) max_val = 10**n-1 sol = SolverFor("QF_FD") # sol = SimpleSolver() # sol = Solver() # sol = SolverFor("LIA") # sol = SolverFor("QF_NIA") # sol = SolverFor("QF_AUFLIA") c,x,y,a,b = Ints("c x y a b") sol.add(c >= 10**(n-2), c <= 10**(n-1)-1) sol.add(x >= min_val, x <= max_val) sol.add(y >= min_val, y <= max_val) sol.add(a >= 1, a <= 9) sol.add(b >= 1, b <= 9) # Connect the variables sol.add(x == c + a*10**(n-1)) sol.add(y == 10*c + b) # sol.add(a == 17, b == 33) # The division # x/y = a/b # converted to multiplication sol.add(x*b == a*y) sol.add(x != y) # solution and search num_solutions = 0 num_repeating_sols = 0 while sol.check() == sat: num_solutions += 1 mod = sol.model() xx = mod.eval(x).as_long() yy = mod.eval(y).as_long() aa = mod.eval(a).as_long() bb = mod.eval(b).as_long() print(f"{xx}/{yy} = {aa}/{bb}") # Skip numbers with less than 5 digits # since they cannot have a repeating digit of .(..)(..) if n >= 5: pattern = find_repeating_pattern(str(xx)) if pattern == "": non_repeating.append([n,xx,yy,aa,bb,is_prime(n)]) num_repeating_sols += 1 ratio_numbers.append((aa,bb,n)) print(f"pattern:{pattern} len:{len(pattern)}\n") # Get new solutions sol.add( Or( x != xx )) t1 = time.time() print(f"{n} num_solutions:{num_solutions} time:{t1-t0}s is_prime:{is_prime(n)} num_repeating_sols:{num_repeating_sols}") # n=2..100 takes 49.9s for n in range(2,100+1): print("n:",n) shifted_division2(n) print(flush=True) # shifted_division2(113) # shifted_division2(234) # Finding the 6 solutions took 2min45s # shifted_division2(1234) # Finding 23 solutions in 2min43.20s # shifted_division2(1231) # Found the 8 solution in 1h43min06.77s # shifted_division2(2345) # This yieds a segmentation fault (after 1min35s) # shifted_division2(12345) print("non_repeating solutions (for x):") for r in non_repeating: print(r) print(f"ratio numbers (len: {len(ratio_numbers)})") for r in sorted(ratio_numbers): print(r)