[Math] Project Euler 142 and Google OR-tools

The problem: Find the smallest x + y + z with integers x > y > z > 0 such that x + y, x - y, x + z, x - z, y + z, y - z are all perfect squares.

The solution using 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")

  solver.Add(x>y)
  solver.Add(y>z)
  solver.Add(z>0)
  solver.Add(a1>0)
  solver.Add(a2>0)
  solver.Add(a3>0)
  solver.Add(a4>0)
  solver.Add(a5>0)
  solver.Add(a6>0)
  solver.Add(x + y == a1*a1)
  solver.Add(x - y == a2*a2)
  solver.Add(x + z == a3*a3)
  solver.Add(x - z == a4*a4)
  solver.Add(y + z == a5*a5)
  solver.Add(y - z == a6*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.)

List of my other blog posts.

Subscribe to my news feed,

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.