Project Euler 164: "How many 20 digit numbers n (without any leading zero) exist such that no three consecutive digits of n have a sum greater than 9?"
The problem above could be solved using SMT solver like z3, but there are too much solutions to enumerate. SAT/SMT is not good in model/solution enumeration/counting (yet?) So I tried Google OR-tools.
#!/usr/bin/python3
import sys, time
from ortools.constraint_solver import pywrapcp
def main(digits_total):
start_t=time.time()
solver = pywrapcp.Solver("...")
# declare variables
x = [solver.IntVar(0, 9, "x%i" % i) for i in range(digits_total)]
for i in range(digits_total-2):
solver.Add(x[i+0]+x[i+1]+x[i+2]<=9)
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(digits_total)])
solutions+=1
solver.EndSearch()
finish_t=time.time()
print(f"{digits_total=} {solutions=} seconds spent: {int(finish_t-start_t)}")
for i in range(3, 20+1):
main(i)
It enumerates solutions fastly. Faster than SAT/SMT solvers. But slows down gradually:
digits_total=3 solutions=220 seconds spent: 0 digits_total=4 solutions=1210 seconds spent: 0 digits_total=5 solutions=6655 seconds spent: 0 digits_total=6 solutions=34243 seconds spent: 0 digits_total=7 solutions=180829 seconds spent: 0 digits_total=8 solutions=963886 seconds spent: 0 digits_total=9 solutions=5093737 seconds spent: 5 digits_total=10 solutions=26932543 seconds spent: 27 digits_total=11 solutions=142701909 seconds spent: 149 digits_total=12 solutions=755538278 seconds spent: 824 digits_total=13 solutions=3999038946 seconds spent: 4104
I cheated and tried to find these numbers on OEIS and found this:
A241615 Number of length n+2 0..9 arrays with no consecutive three elements summing to more than 9 220, 1210, 6655, 34243, 180829, 963886, 5093737, 26932543, 142701909, 755538278, 3999038946, 21172904049, 112098384491, 593455432350, 3141868198978, 16633824615067, 88062718713584, 466221475528171, 2468274573927916
I tried several numbers on projecteuler.net website with no luck. Ouch. I forgot about this clause in problem definition: "(without any leading zero)".
So I added that constraint:
solver.Add(x[0]!=0)
Now results are different:
digits_total=3 solutions=165 seconds spent: 0 digits_total=4 solutions=990 seconds spent: 0 digits_total=5 solutions=5445 seconds spent: 0 digits_total=6 solutions=27588 seconds spent: 0 digits_total=7 solutions=146586 seconds spent: 0 digits_total=8 solutions=783057 seconds spent: 0 digits_total=9 solutions=4129851 seconds spent: 4 digits_total=10 solutions=21838806 seconds spent: 23 digits_total=11 solutions=115769366 seconds spent: 118 digits_total=12 solutions=612836369 seconds spent: 627
... but still it works too slow to count to digits_total=20.
But I started to suspect something.
First two numbers on OEIS A241615: 220, 1210. And 1210-220=990 Second and third numbers: 1210, 6655. And 6655-1210=5445. These are solutions from my second program.
Let's try other pairs:
#!/usr/bin/python3
A241615=[
220, 1210, 6655, 34243, 180829, 963886, 5093737, 26932543, 142701909,
755538278, 3999038946, 21172904049, 112098384491, 593455432350,
3141868198978, 16633824615067, 88062718713584, 466221475528171,
2468274573927916, 13067553701179851]
for i in range(1, len(A241615)-1):
print (i, A241615[i+1]-A241615[i])
1 5445 2 27588 3 146586 4 783057 5 4129851 6 21838806 7 115769366 8 612836369 9 3243500668 10 17173865103 11 90925480442 12 481357047859 13 2548412766628 14 13491956416089 15 71428894098517 16 378158756814587 17 2002053098399745 18 10599279127251935
And the winner is (picked from this list): 378158756814587.
It's indeed so: we 'remove' solutions starting with zero. And solutions count without first zero number is just previous entry. Leading zero doesn't break that 'sum of 3 any consecutive numbers <= 9' constraint, because adding zero doesn't change anything.
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.