## [Math] Project Euler 158: solving it using Google OR-tools

Project Euler 158: Taking three different letters from the 26 letters of the alphabet, character strings of length three can be formed.
Examples are 'abc', 'hat' and 'zyx'.
When we study these three examples we see that for 'abc' two characters come lexicographically after its neighbour to the left.
For 'hat' there is exactly one character that comes lexicographically after its neighbour to the left. For 'zyx' there are zero characters that come lexicographically after its neighbour to the left.
In all there are 10400 strings of length 3 for which exactly one character comes lexicographically after its neighbour to the left.
We now consider strings of n ≤ 26 different characters from the alphabet.
For every n, p(n) is the number of strings of length n for which exactly one character comes lexicographically after its neighbour to the left.
What is the maximum value of p(n)?

Yet again, as it often happens with my solutions, it could be solved much easier, maybe even using paper and pencil. My solution worked for ~4 days on 16 ARM CPU cores, however, I spent only ~10-15 minutes on coding, and my knowledge of combinatorics is low.

#!/usr/bin/python3

import sys, time
from ortools.constraint_solver import pywrapcp

def main(chars_total, LT_pair_start):
print(f"main() {chars_total=} {LT_pair_start=}")

start_t=time.time()
solver = pywrapcp.Solver("...")

# declare variables
x = [solver.IntVar(0, 26-1, "x%i" % i) for i in range(chars_total)]

for i in range(chars_total-1):
if i==LT_pair_start:
else:

# all distinct
for i in range(chars_total):
for j in range(i+1, chars_total):

solution = solver.Assignment()

db = solver.Phase(x, solver.CHOOSE_MIN_SIZE_LOWEST_MAX,
solver.ASSIGN_MIN_VALUE)

solver.NewSearch(db)
solutions = 0
while solver.NextSolution():
#print("x: ", [x[i].Value() for i in range(chars_total)])
solutions+=1
solver.EndSearch()

finish_t=time.time()
print(f"chars_total, LT_pair_start, solutions = {chars_total} {LT_pair_start} {solutions}")
sys.stdout.flush()
return solutions

def p(n):
chars_total=n
solutions_total=0
for i in range(chars_total-1):
solutions_total+=main(chars_total, i)

print (f"p({n=}) {solutions_total=}")
return solutions_total

# tests:
assert main(chars_total=26, LT_pair_start=0)==25
assert main(chars_total=26, LT_pair_start=24)==25

assert main(chars_total=26, LT_pair_start=1)==324
assert main(chars_total=26, LT_pair_start=23)==324

assert main(chars_total=26, LT_pair_start=2)==2599
assert main(chars_total=26, LT_pair_start=22)==2599

assert p(3)==10400

#p(6)
#p(25)

#for n in range(26+1):
#    p(n)

"""
def gen_all():
for chars_total in range(26+1):
for i in range(chars_total-1):
log_name="log_%d_%d" % (chars_total, i)
print ("./PE158.py", chars_total, i, " > ", log_name)

gen_all()
"""

import sys

main(int(sys.argv[1]), int(sys.argv[2]))


LT_pair is 'less-than pair', must be present only once in 'chain'. It's to be run using GNU parallel -- for some reason, I couldn't make it work as multi-threaded program, maybe the problem is in the ortools module? Who knows.

chars_total, LT_pair_start, solutions = 10 0 47805615
chars_total, LT_pair_start, solutions = 10 1 233716340
chars_total, LT_pair_start, solutions = 10 2 632096465
chars_total, LT_pair_start, solutions = 10 3 1110152615
chars_total, LT_pair_start, solutions = 10 4 1333245485
chars_total, LT_pair_start, solutions = 10 5 1110152615
chars_total, LT_pair_start, solutions = 10 6 632096465
chars_total, LT_pair_start, solutions = 10 7 233716340
chars_total, LT_pair_start, solutions = 10 8 47805615
chars_total, LT_pair_start, solutions = 11 0 77261600
chars_total, LT_pair_start, solutions = 11 1 417212640
chars_total, LT_pair_start, solutions = 11 2 1267090240
chars_total, LT_pair_start, solutions = 11 3 2541906640
chars_total, LT_pair_start, solutions = 11 4 3561759760
chars_total, LT_pair_start, solutions = 11 5 3561759760
chars_total, LT_pair_start, solutions = 11 6 2541906640
chars_total, LT_pair_start, solutions = 11 7 1267090240
chars_total, LT_pair_start, solutions = 11 8 417212640
chars_total, LT_pair_start, solutions = 11 9 77261600
chars_total, LT_pair_start, solutions = 12 0 106234700
chars_total, LT_pair_start, solutions = 12 10 106234700
chars_total, LT_pair_start, solutions = 12 1 627750500
chars_total, LT_pair_start, solutions = 12 2 2115036300
chars_total, LT_pair_start, solutions = 12 3 4770903800
chars_total, LT_pair_start, solutions = 12 4 7639240700
chars_total, LT_pair_start, solutions = 12 5 8914057100
chars_total, LT_pair_start, solutions = 12 6 7639240700
chars_total, LT_pair_start, solutions = 12 7 4770903800
chars_total, LT_pair_start, solutions = 12 8 2115036300
chars_total, LT_pair_start, solutions = 12 9 627750500
chars_total, LT_pair_start, solutions = 13 0 124807200
chars_total, LT_pair_start, solutions = 13 10 800846200
chars_total, LT_pair_start, solutions = 13 11 124807200
chars_total, LT_pair_start, solutions = 13 1 800846200
chars_total, LT_pair_start, solutions = 13 2 2964171000
chars_total, LT_pair_start, solutions = 13 3 7426028400
chars_total, LT_pair_start, solutions = 13 4 13375171600
chars_total, LT_pair_start, solutions = 13 5 17837029000
chars_total, LT_pair_start, solutions = 13 6 17837029000
chars_total, LT_pair_start, solutions = 13 7 13375171600
chars_total, LT_pair_start, solutions = 13 8 7426028400
chars_total, LT_pair_start, solutions = 13 9 2964171000
chars_total, LT_pair_start, solutions = 14 0 125550100
chars_total, LT_pair_start, solutions = 14 10 3505745100
chars_total, LT_pair_start, solutions = 14 11 869193000
chars_total, LT_pair_start, solutions = 14 12 125550100
chars_total, LT_pair_start, solutions = 14 1 869193000
chars_total, LT_pair_start, solutions = 14 2 3505745100
chars_total, LT_pair_start, solutions = 14 3 9657700000
chars_total, LT_pair_start, solutions = 14 4 19325057700
chars_total, LT_pair_start, solutions = 14 5 28992415400
chars_total, LT_pair_start, solutions = 14 6 33135568700
chars_total, LT_pair_start, solutions = 14 7 28992415400
chars_total, LT_pair_start, solutions = 14 8 19325057700
chars_total, LT_pair_start, solutions = 14 9 9657700000
chars_total, LT_pair_start, solutions = 15 0 108166240
chars_total, LT_pair_start, solutions = 15 10 10538482240
chars_total, LT_pair_start, solutions = 15 11 3507676640
chars_total, LT_pair_start, solutions = 15 12 803520640
chars_total, LT_pair_start, solutions = 15 13 108166240
chars_total, LT_pair_start, solutions = 15 1 803520640
chars_total, LT_pair_start, solutions = 15 2 3507676640
chars_total, LT_pair_start, solutions = 15 3 10538482240
chars_total, LT_pair_start, solutions = 15 4 23193932320
chars_total, LT_pair_start, solutions = 15 5 38661704640
chars_total, LT_pair_start, solutions = 15 6 49710113440
chars_total, LT_pair_start, solutions = 15 7 49710113440
chars_total, LT_pair_start, solutions = 15 8 38661704640
chars_total, LT_pair_start, solutions = 15 9 23193932320
chars_total, LT_pair_start, solutions = 16 0 79676025
chars_total, LT_pair_start, solutions = 16 10 23196346745
chars_total, LT_pair_start, solutions = 16 11 9662045965
chars_total, LT_pair_start, solutions = 16 12 2969259865
chars_total, LT_pair_start, solutions = 16 13 632096465
chars_total, LT_pair_start, solutions = 16 14 79676025
chars_total, LT_pair_start, solutions = 16 1 632096465
chars_total, LT_pair_start, solutions = 16 2 2969259865
chars_total, LT_pair_start, solutions = 16 3 9662045965
chars_total, LT_pair_start, solutions = 16 4 23196346745
chars_total, LT_pair_start, solutions = 16 5 42531062145
chars_total, LT_pair_start, solutions = 16 6 60760936665
chars_total, LT_pair_start, solutions = 16 7 68356717715
chars_total, LT_pair_start, solutions = 16 8 60760936665
chars_total, LT_pair_start, solutions = 16 9 42531062145
chars_total, LT_pair_start, solutions = 17 0 49992800
chars_total, LT_pair_start, solutions = 17 10 38666306250
chars_total, LT_pair_start, solutions = 17 11 19331590850
chars_total, LT_pair_start, solutions = 17 12 7433304450
chars_total, LT_pair_start, solutions = 17 13 2121569450
chars_total, LT_pair_start, solutions = 17 1 421814250
chars_total, LT_pair_start, solutions = 17 14 421814250
chars_total, LT_pair_start, solutions = 17 15 49992800
chars_total, LT_pair_start, solutions = 17 2 2121569450
chars_total, LT_pair_start, solutions = 17 3 7433304450
chars_total, LT_pair_start, solutions = 17 4 19331590850
chars_total, LT_pair_start, solutions = 17 5 38666306250
chars_total, LT_pair_start, solutions = 17 6 60763123850
chars_total, LT_pair_start, solutions = 17 7 75954685950
chars_total, LT_pair_start, solutions = 17 8 75954685950
chars_total, LT_pair_start, solutions = 17 9 60763123850
chars_total, LT_pair_start, solutions = 18 0 26558675
chars_total, LT_pair_start, solutions = 18 10 49716277325
chars_total, LT_pair_start, solutions = 18 11 29000510825
chars_total, LT_pair_start, solutions = 18 12 13384009925
chars_total, LT_pair_start, solutions = 18 1 237465800
chars_total, LT_pair_start, solutions = 18 13 4778999225
chars_total, LT_pair_start, solutions = 18 14 1273254125
chars_total, LT_pair_start, solutions = 18 15 237465800
chars_total, LT_pair_start, solutions = 18 16 26558675
chars_total, LT_pair_start, solutions = 18 2 1273254125
chars_total, LT_pair_start, solutions = 18 3 4778999225
chars_total, LT_pair_start, solutions = 18 4 13384009925
chars_total, LT_pair_start, solutions = 18 5 29000510825
chars_total, LT_pair_start, solutions = 18 6 49716277325
chars_total, LT_pair_start, solutions = 18 7 68360467175
chars_total, LT_pair_start, solutions = 18 8 75956248225
chars_total, LT_pair_start, solutions = 18 9 68360467175
chars_total, LT_pair_start, solutions = 19 0 11840400
chars_total, LT_pair_start, solutions = 19 10 49717181800
chars_total, LT_pair_start, solutions = 19 1 111826000
chars_total, LT_pair_start, solutions = 19 11 33144568600
chars_total, LT_pair_start, solutions = 19 12 17846771800
chars_total, LT_pair_start, solutions = 19 13 7648240600
chars_total, LT_pair_start, solutions = 19 14 2548975000
chars_total, LT_pair_start, solutions = 19 15 636750400
chars_total, LT_pair_start, solutions = 19 16 111826000
chars_total, LT_pair_start, solutions = 19 17 11840400
chars_total, LT_pair_start, solutions = 19 2 636750400
chars_total, LT_pair_start, solutions = 19 3 2548975000
chars_total, LT_pair_start, solutions = 19 4 7648240600
chars_total, LT_pair_start, solutions = 19 5 17846771800
chars_total, LT_pair_start, solutions = 19 6 33144568600
chars_total, LT_pair_start, solutions = 19 7 49717181800
chars_total, LT_pair_start, solutions = 19 8 60765590600
chars_total, LT_pair_start, solutions = 19 9 60765590600
chars_total, LT_pair_start, solutions = 20 0 4374370
chars_total, LT_pair_start, solutions = 20 10 38669200570
chars_total, LT_pair_start, solutions = 20 11 29001842870
chars_total, LT_pair_start, solutions = 20 12 17847199370
chars_total, LT_pair_start, solutions = 20 13 8923484570
chars_total, LT_pair_start, solutions = 20 1 43513470
chars_total, LT_pair_start, solutions = 20 14 3569255690
chars_total, LT_pair_start, solutions = 20 15 1115234120
chars_total, LT_pair_start, solutions = 20 16 262231970
chars_total, LT_pair_start, solutions = 20 17 43513470
chars_total, LT_pair_start, solutions = 20 18 4374370
chars_total, LT_pair_start, solutions = 20 2 262231970
chars_total, LT_pair_start, solutions = 20 3 1115234120
chars_total, LT_pair_start, solutions = 2 0 325
chars_total, LT_pair_start, solutions = 20 4 3569255690
chars_total, LT_pair_start, solutions = 20 5 8923484570
chars_total, LT_pair_start, solutions = 20 6 17847199370
chars_total, LT_pair_start, solutions = 20 7 29001842870
chars_total, LT_pair_start, solutions = 20 8 38669200570
chars_total, LT_pair_start, solutions = 20 9 42536143650
chars_total, LT_pair_start, solutions = 21 0 1315600
chars_total, LT_pair_start, solutions = 21 10 23201592700
chars_total, LT_pair_start, solutions = 21 11 19334649620
chars_total, LT_pair_start, solutions = 21 1 13748020
chars_total, LT_pair_start, solutions = 21 12 13385506420
chars_total, LT_pair_start, solutions = 21 13 7648832620
chars_total, LT_pair_start, solutions = 21 14 3569420140
chars_total, LT_pair_start, solutions = 21 15 1338491440
chars_total, LT_pair_start, solutions = 21 16 393627520
chars_total, LT_pair_start, solutions = 21 17 87421620
chars_total, LT_pair_start, solutions = 21 18 13748020
chars_total, LT_pair_start, solutions = 21 19 1315600
chars_total, LT_pair_start, solutions = 21 2 87421620
chars_total, LT_pair_start, solutions = 21 3 393627520
chars_total, LT_pair_start, solutions = 21 4 1338491440
chars_total, LT_pair_start, solutions = 21 5 3569420140
chars_total, LT_pair_start, solutions = 21 6 7648832620
chars_total, LT_pair_start, solutions = 21 7 13385506420
chars_total, LT_pair_start, solutions = 21 8 19334649620
chars_total, LT_pair_start, solutions = 21 9 23201592700
chars_total, LT_pair_start, solutions = 22 0 313950
chars_total, LT_pair_start, solutions = 22 10 10546193450
chars_total, LT_pair_start, solutions = 22 11 9667342750
chars_total, LT_pair_start, solutions = 22 12 7436414050
chars_total, LT_pair_start, solutions = 22 1 3438500
chars_total, LT_pair_start, solutions = 22 13 4780546550
chars_total, LT_pair_start, solutions = 22 14 2549617850
chars_total, LT_pair_start, solutions = 22 15 1115449400
chars_total, LT_pair_start, solutions = 22 16 393678350
chars_total, LT_pair_start, solutions = 22 17 109344300
chars_total, LT_pair_start, solutions = 22 18 23008050
chars_total, LT_pair_start, solutions = 22 19 3438500
chars_total, LT_pair_start, solutions = 22 20 313950
chars_total, LT_pair_start, solutions = 22 2 23008050
chars_total, LT_pair_start, solutions = 22 3 109344300
chars_total, LT_pair_start, solutions = 22 4 393678350
chars_total, LT_pair_start, solutions = 22 5 1115449400
chars_total, LT_pair_start, solutions = 22 6 2549617850
chars_total, LT_pair_start, solutions = 22 7 4780546550
chars_total, LT_pair_start, solutions = 22 8 7436414050
chars_total, LT_pair_start, solutions = 22 9 9667342750
chars_total, LT_pair_start, solutions = 23 0 57200
chars_total, LT_pair_start, solutions = 23 10 3515400200
chars_total, LT_pair_start, solutions = 23 11 3515400200
chars_total, LT_pair_start, solutions = 23 12 2974569000
chars_total, LT_pair_start, solutions = 23 13 2124691400
chars_total, LT_pair_start, solutions = 23 14 1274813800
chars_total, LT_pair_start, solutions = 23 15 637405600
chars_total, LT_pair_start, solutions = 23 16 262459600
chars_total, LT_pair_start, solutions = 23 1 655200
chars_total, LT_pair_start, solutions = 23 17 87484800
chars_total, LT_pair_start, solutions = 23 18 23020400
chars_total, LT_pair_start, solutions = 23 19 4602000
chars_total, LT_pair_start, solutions = 23 20 655200
chars_total, LT_pair_start, solutions = 23 21 57200
chars_total, LT_pair_start, solutions = 23 2 4602000
chars_total, LT_pair_start, solutions = 23 3 23020400
chars_total, LT_pair_start, solutions = 23 4 87484800
chars_total, LT_pair_start, solutions = 23 5 262459600
chars_total, LT_pair_start, solutions = 23 6 637405600
chars_total, LT_pair_start, solutions = 23 7 1274813800
chars_total, LT_pair_start, solutions = 23 8 2124691400
chars_total, LT_pair_start, solutions = 23 9 2974569000
chars_total, LT_pair_start, solutions = 24 0 7475
chars_total, LT_pair_start, solutions = 24 10 811246475
chars_total, LT_pair_start, solutions = 24 11 878850375
chars_total, LT_pair_start, solutions = 24 12 811246475
chars_total, LT_pair_start, solutions = 24 13 637407875
chars_total, LT_pair_start, solutions = 24 14 424938475
chars_total, LT_pair_start, solutions = 24 15 239027750
chars_total, LT_pair_start, solutions = 24 16 112483475
chars_total, LT_pair_start, solutions = 24 17 43743375
chars_total, LT_pair_start, solutions = 24 18 13813475
chars_total, LT_pair_start, solutions = 24 1 89375
chars_total, LT_pair_start, solutions = 24 19 3453125
chars_total, LT_pair_start, solutions = 24 20 657475
chars_total, LT_pair_start, solutions = 24 21 89375
chars_total, LT_pair_start, solutions = 24 22 7475
chars_total, LT_pair_start, solutions = 24 2 657475
chars_total, LT_pair_start, solutions = 24 3 3453125
chars_total, LT_pair_start, solutions = 24 4 13813475
chars_total, LT_pair_start, solutions = 24 5 43743375
chars_total, LT_pair_start, solutions = 24 6 112483475
chars_total, LT_pair_start, solutions = 24 7 239027750
chars_total, LT_pair_start, solutions = 24 8 424938475
chars_total, LT_pair_start, solutions = 24 9 637407875
chars_total, LT_pair_start, solutions = 25 0 624
chars_total, LT_pair_start, solutions = 25 10 115892374
chars_total, LT_pair_start, solutions = 25 11 135207774
chars_total, LT_pair_start, solutions = 25 12 135207774
chars_total, LT_pair_start, solutions = 25 13 115892374
chars_total, LT_pair_start, solutions = 25 14 84987734
chars_total, LT_pair_start, solutions = 25 15 53117324
chars_total, LT_pair_start, solutions = 25 16 28120924
chars_total, LT_pair_start, solutions = 25 17 12498174
chars_total, LT_pair_start, solutions = 25 1 7774
chars_total, LT_pair_start, solutions = 25 18 4604574
chars_total, LT_pair_start, solutions = 25 19 1381354
chars_total, LT_pair_start, solutions = 25 20 328874
chars_total, LT_pair_start, solutions = 25 21 59774
chars_total, LT_pair_start, solutions = 25 22 7774
chars_total, LT_pair_start, solutions = 25 23 624
chars_total, LT_pair_start, solutions = 25 2 59774
chars_total, LT_pair_start, solutions = 25 3 328874
chars_total, LT_pair_start, solutions = 25 4 1381354
chars_total, LT_pair_start, solutions = 25 5 4604574
chars_total, LT_pair_start, solutions = 25 6 12498174
chars_total, LT_pair_start, solutions = 25 7 28120924
chars_total, LT_pair_start, solutions = 25 8 53117324
chars_total, LT_pair_start, solutions = 25 9 84987734
chars_total, LT_pair_start, solutions = 26 0 25
chars_total, LT_pair_start, solutions = 26 10 7726159
chars_total, LT_pair_start, solutions = 26 11 9657699
chars_total, LT_pair_start, solutions = 26 12 10400599
chars_total, LT_pair_start, solutions = 26 1 324
chars_total, LT_pair_start, solutions = 26 13 9657699
chars_total, LT_pair_start, solutions = 26 14 7726159
chars_total, LT_pair_start, solutions = 26 15 5311734
chars_total, LT_pair_start, solutions = 26 16 3124549
chars_total, LT_pair_start, solutions = 26 17 1562274
chars_total, LT_pair_start, solutions = 26 18 657799
chars_total, LT_pair_start, solutions = 26 19 230229
chars_total, LT_pair_start, solutions = 26 20 65779
chars_total, LT_pair_start, solutions = 26 21 14949
chars_total, LT_pair_start, solutions = 26 22 2599
chars_total, LT_pair_start, solutions = 26 2 2599
chars_total, LT_pair_start, solutions = 26 23 324
chars_total, LT_pair_start, solutions = 26 24 25
chars_total, LT_pair_start, solutions = 26 3 14949
chars_total, LT_pair_start, solutions = 26 4 65779
chars_total, LT_pair_start, solutions = 26 5 230229
chars_total, LT_pair_start, solutions = 26 6 657799
chars_total, LT_pair_start, solutions = 26 7 1562274
chars_total, LT_pair_start, solutions = 26 8 3124549
chars_total, LT_pair_start, solutions = 26 9 5311734
chars_total, LT_pair_start, solutions = 3 0 5200
chars_total, LT_pair_start, solutions = 3 1 5200
chars_total, LT_pair_start, solutions = 4 0 44850
chars_total, LT_pair_start, solutions = 4 1 74750
chars_total, LT_pair_start, solutions = 4 2 44850
chars_total, LT_pair_start, solutions = 5 0 263120
chars_total, LT_pair_start, solutions = 5 1 592020
chars_total, LT_pair_start, solutions = 5 2 592020
chars_total, LT_pair_start, solutions = 5 3 263120
chars_total, LT_pair_start, solutions = 6 0 1151150
chars_total, LT_pair_start, solutions = 6 1 3223220
chars_total, LT_pair_start, solutions = 6 2 4374370
chars_total, LT_pair_start, solutions = 6 3 3223220
chars_total, LT_pair_start, solutions = 6 4 1151150
chars_total, LT_pair_start, solutions = 7 0 3946800
chars_total, LT_pair_start, solutions = 7 1 13156000
chars_total, LT_pair_start, solutions = 7 2 22365200
chars_total, LT_pair_start, solutions = 7 3 22365200
chars_total, LT_pair_start, solutions = 7 4 13156000
chars_total, LT_pair_start, solutions = 7 5 3946800
chars_total, LT_pair_start, solutions = 8 0 10935925
chars_total, LT_pair_start, solutions = 8 1 42181425
chars_total, LT_pair_start, solutions = 8 2 85925125
chars_total, LT_pair_start, solutions = 8 3 107796975
chars_total, LT_pair_start, solutions = 8 4 85925125
chars_total, LT_pair_start, solutions = 8 5 42181425
chars_total, LT_pair_start, solutions = 8 6 10935925
chars_total, LT_pair_start, solutions = 9 0 24996400
chars_total, LT_pair_start, solutions = 9 1 109359250
chars_total, LT_pair_start, solutions = 9 2 259337650
chars_total, LT_pair_start, solutions = 9 3 390568750
chars_total, LT_pair_start, solutions = 9 4 390568750
chars_total, LT_pair_start, solutions = 9 5 259337650
chars_total, LT_pair_start, solutions = 9 6 109359250
chars_total, LT_pair_start, solutions = 9 7 24996400


Maximal solutions count is 7.5e10 -- not bad!

Yet again, a tool like Google OR-tools compensated my bad math experience.

Also, a symmetry is clearly visible here:

chars_total, LT_pair_start, solutions = 16 0  79676025
chars_total, LT_pair_start, solutions = 16 1  632096465
chars_total, LT_pair_start, solutions = 16 2  2969259865
chars_total, LT_pair_start, solutions = 16 3  9662045965
chars_total, LT_pair_start, solutions = 16 4  23196346745
chars_total, LT_pair_start, solutions = 16 5  42531062145
chars_total, LT_pair_start, solutions = 16 6  60760936665
chars_total, LT_pair_start, solutions = 16 7  68356717715
chars_total, LT_pair_start, solutions = 16 8  60760936665
chars_total, LT_pair_start, solutions = 16 9  42531062145
chars_total, LT_pair_start, solutions = 16 10 23196346745
chars_total, LT_pair_start, solutions = 16 11 9662045965
chars_total, LT_pair_start, solutions = 16 12 2969259865
chars_total, LT_pair_start, solutions = 16 13 632096465
chars_total, LT_pair_start, solutions = 16 14 79676025


Of course, it should be taken into account and execution time would be approximately halved. But I was too lazy for this.

###### (the post first published at 20240813.)

Yes, I know about these lousy Disqus ads. Please use adblocker. I would consider to subscribe to 'pro' version of Disqus if the signal/noise ratio in comments would be good enough.