## [Math] Project Euler 142 and Google OR-tools

#!/usr/bin/python3

# pip install ortools
# https://pypi.org/project/ortools/
from ortools.constraint_solver import pywrapcp

def main():
solver = pywrapcp.Solver("PE_142")

max_limit=1000000
max_limit_sqr=(max_limit*2)**2

x=solver.IntVar(0, max_limit, "x")
y=solver.IntVar(0, max_limit, "y")
z=solver.IntVar(0, max_limit, "z")
a1=solver.IntVar(0, max_limit_sqr, "a1")
a2=solver.IntVar(0, max_limit_sqr, "a2")
a3=solver.IntVar(0, max_limit_sqr, "a3")
a4=solver.IntVar(0, max_limit_sqr, "a4")
a5=solver.IntVar(0, max_limit_sqr, "a5")
a6=solver.IntVar(0, max_limit_sqr, "a6")

# objective
objective = solver.Minimize(x+z+y, 1)

solution = solver.Assignment()

db = solver.Phase([x,y,z],
solver.CHOOSE_MIN_SIZE_LOWEST_MAX,
solver.ASSIGN_MIN_VALUE)

solver.NewSearch(db, [objective])
assert solver.NextSolution()==True
print("x: ", x.Value())
print("y: ", y.Value())
print("z: ", z.Value())
print()
solver.EndSearch()

print("failures:", solver.Failures())
print("branches:", solver.Branches())
print("WallTime:", solver.WallTime())

main()

% my_time.py ./1.py
['./1.py']
x:  434657
y:  420968
z:  150568

failures: 215193
branches: 430387
WallTime: 457060
['/home/i/dotfiles/bin/my_time.py', './1.py']
seconds:  457
or:  7m37s


Thanks to HÃ¥kan Kjellerstrand for his snippets, including those for OR-tools, which are so easy to study and modify...

Z3 SMT solver should work as well, but don't.

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

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.