""" 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. Also, see an animation of this at https://twitter.com/ScienceMagician/status/1485613903623200776 Here are all solutions for n=2..10 n: 2 min_val: 10 max_val: 99 26/65 = 2/5 49/98 = 4/8 19/95 = 1/5 16/64 = 1/4 num_solutions: 4 n: 3 min_val: 100 max_val: 999 499/998 = 4/8 654/545 = 6/5 484/847 = 4/7 742/424 = 7/4 199/995 = 1/5 166/664 = 1/4 266/665 = 2/5 num_solutions: 7 n: 4 min_val: 1000 max_val: 9999 4999/9998 = 4/8 2666/6665 = 2/5 4324/3243 = 4/3 1999/9995 = 1/5 1666/6664 = 1/4 8648/6486 = 8/6 num_solutions: 6 n: 5 min_val: 10000 max_val: 99999 74242/42424 = 7/4 26666/66665 = 2/5 48484/84847 = 4/7 16666/66664 = 1/4 65454/54545 = 6/5 19999/99995 = 1/5 49999/99998 = 4/8 num_solutions: 7 n: 6 min_val: 100000 max_val: 999999 166666/666664 = 1/4 266666/666665 = 2/5 499999/999998 = 4/8 987804/878048 = 9/8 199999/999995 = 1/5 num_solutions: 5 n: 7 min_val: 1000000 max_val: 9999999 6923076/9230768 = 6/8 7538461/5384615 = 7/5 1428571/4285713 = 1/3 4102564/1025641 = 4/1 8311688/3116883 = 8/3 8205128/2051282 = 8/2 8648648/6486486 = 8/6 4848484/8484847 = 4/7 6545454/5454545 = 6/5 1999999/9999995 = 1/5 4571428/5714285 = 4/5 4324324/3243243 = 4/3 3461538/4615384 = 3/4 2666666/6666665 = 2/5 2857142/8571426 = 2/6 6428571/4285714 = 6/4 4999999/9999998 = 4/8 1666666/6666664 = 1/4 5952380/9523808 = 5/8 7424242/4242424 = 7/4 num_solutions: 20 n: 8 min_val: 10000000 max_val: 99999999 26666666/66666665 = 2/5 49999999/99999998 = 4/8 16666666/66666664 = 1/4 19999999/99999995 = 1/5 num_solutions: 4 n: 9 min_val: 100000000 max_val: 999999999 876712328/767123287 = 8/7 484848484/848484847 = 4/7 742424242/424242424 = 7/4 199999999/999999995 = 1/5 166666666/666666664 = 1/4 266666666/666666665 = 2/5 499999999/999999998 = 4/8 654545454/545454545 = 6/5 num_solutions: 8 And some other sizes: n:17 (it took 3min11s) 87671232876712328/76712328767123287 = 8/7 95294117647058823/52941176470588235 = 9/5 65454545454545454/54545454545454545 = 6/5 47058823529411764/70588235294117646 = 4/6 48484848484848484/84848484848484847 = 4/7 19999999999999999/99999999999999995 = 1/5 49999999999999999/99999999999999998 = 4/8 26666666666666666/66666666666666665 = 2/5 16666666666666666/66666666666666664 = 1/4 74242424242424242/42424242424242424 = 7/4 23529411764705882/35294117647058823 = 2/3 num_solutions: 11 n:18 199999999999999999/999999999999999995 = 1/5 499999999999999999/999999999999999998 = 4/8 166666666666666666/666666666666666664 = 1/4 266666666666666666/666666666666666665 = 2/5 num_solutions: 4 n:19 7424242424242424242/4242424242424242424 = 7/4 5952380952380952380/9523809523809523808 = 5/8 4571428571428571428/5714285714285714285 = 4/5 4999999999999999999/9999999999999999998 = 4/8 1999999999999999999/9999999999999999995 = 1/5 3461538461538461538/4615384615384615384 = 3/4 4102564102564102564/1025641025641025641 = 4/1 1666666666666666666/6666666666666666664 = 1/4 6923076923076923076/9230769230769230768 = 6/8 8648648648648648648/6486486486486486486 = 8/6 4210526315789473684/2105263157894736842 = 4/2 2857142857142857142/8571428571428571426 = 2/6 6428571428571428571/4285714285714285714 = 6/4 4324324324324324324/3243243243243243243 = 4/3 6545454545454545454/5454545454545454545 = 6/5 6315789473684210526/3157894736842105263 = 6/3 1428571428571428571/4285714285714285713 = 1/3 8421052631578947368/4210526315789473684 = 8/4 2666666666666666666/6666666666666666665 = 2/5 7538461538461538461/5384615384615384615 = 7/5 2105263157894736842/1052631578947368421 = 2/1 8311688311688311688/3116883116883116883 = 8/3 8205128205128205128/2051282051282051282 = 8/2 4848484848484848484/8484848484848484847 = 4/7 num_solutions: 24 n:27 742424242424242424242424242/424242424242424242424242424 = 7/4 266666666666666666666666666/666666666666666666666666665 = 2/5 679245283018867924528301886/792452830188679245283018867 = 6/7 This model is a port of my Picat model http://hakank.org/picat/shifted_division.pi This Z3 model was written by Hakan Kjellerstrand (hakank@gmail.com) See also my Z3 page: http://hakank.org/z3/ """ from z3 import * # converts a number (s) <-> an array of integers (t) in the specific base. # See toNum.py def toNum(sol, t, s, base): tlen = len(t) sol.add(s == Sum([(base ** (tlen - i - 1)) * t[i] for i in range(tlen)])) def shifted_division(n): min_val = 10**(n-1) max_val = 10**n-1 print(f"n:{n}") # sol = SimpleSolver() # sol = Solver() sol = SolverFor("QF_FD") # sol = SolverFor("QF_NIA") # sol = SolverFor("QF_AUFLIA") x,y = Ints("x y") sol.add(x >= min_val, x <= max_val) sol.add(y >= min_val, y <= max_val) a = [Int(f"a[{i}]") for i in range(n)] b = [Int(f"b[{i}]") for i in range(n)] for i in range(n): sol.add(a[i] >= 0, a[i] <= 9) sol.add(b[i] >= 0, b[i] <= 9) # convert the numbers x and y to array of digits toNum(sol,a,x,10) toNum(sol,b,y,10) # Shift a to b for i in range(1,n): sol.add(a[i] == b[i-1]) # The division # x/y = a(0)/b(n-1) # converted to multiplication sol.add(x*b[n-1] == a[0]*y) sol.add(x != y) # A little help # sol.add(a[0] == 5, b[n-1] == 7) # solution and search num_solutions = 0 while sol.check() == sat: num_solutions += 1 mod = sol.model() xx = mod.eval(x) yy = mod.eval(y) aa = [mod.eval(a[i]) for i in range(n)] bb = [mod.eval(b[i]) for i in range(n)] print(f"{xx}/{yy} = {aa[0]}/{bb[n-1]}") # Get new solutions sol.add( Or( x != xx, y != yy )) print("num_solutions:", num_solutions) # for n in range(2,20): # print("n:",n) # shifted_division(n) # print() # shifted_division(27) shifted_division(127)