A quick solver for https://plus.google.com/101584889282878921052/posts/Fni6x2TTeaS

82000 Solver.py

import tempfile
import os
import subprocess
import functools
import time

JAVA_NAME = 'java'
JAVA_OPTIONS = ['-server', '-Xmx4g', '-jar']
SAT4J_PB = r'C:\Dev\sat4j\sat4j-pb.jar'

def genbasestr(i, b, maxsize, pm='+'):
    basestr = [None]*maxsize
    v = 1
    for x in range(maxsize):
        basestr[x] = "{} x{}".format(v, x + i*maxsize + 1)
        v *= b
    return (" "+pm).join(basestr)

def gen(write, maxsize, bases):
    numVars = len(bases)*maxsize
    numConstraints = len(bases)
    write("* #variable= {} #constraint= {}".format(numVars, numConstraints))
    write("\n")
    print("\t\t", "Generating base {} string...".format(bases[0]))
    basestrZ = genbasestr(0, bases[0], maxsize)
    for i, x in enumerate(bases[1:], 1):
        print("\t\t", "Generating base {} string...".format(x))
        toAdd = genbasestr(i, x, maxsize, '-')
        print("\t\t", "Writing base {} string...".format(x))
        write("{} -{} = 0;".format(basestrZ, toAdd))
        write("\n")
    write("{} >= 2;".format(basestrZ))

def to2d(l, n):
    return [l[i:i+n] for i in range(0, len(l), n)]

def solve(maxsize, bases):
    fd, filename = tempfile.mkstemp(suffix='.pbs', text=True)
    try:
        gen(lambda w: os.write(fd, w.encode()), maxsize, bases)
        print("\t\t", solving)
        os.close(fd)
        startupinfo = None
        if os.name == 'nt':
            startupinfo = subprocess.STARTUPINFO()
            startupinfo.dwFlags |= subprocess.STARTF_USESHOWWINDOW
        proc = subprocess.Popen([JAVA_NAME] + JAVA_OPTIONS + [SAT4J_PB, filename],
                                stdout=subprocess.PIPE, startupinfo=startupinfo)
        sat = None
        var = {}
        for line in proc.stdout:
            line = line.decode('utf-8')
            if line[-1] == '\n':
                line = line[:-1]
            if line.startswith("s"):
                sat = line[2:].strip()
            elif line.startswith("v"):
                for x in line.split(" ")[1:-1]:
                    if "x" in x:
                        var[int(x[x.index("x")+1:])] = not ("-" in x)
            else:
                print("\t\t\t", line)
        temp = [None]*len(var)
        for i,v in var.items():
            temp[i-1] = v
        var = to2d(temp, maxsize)
        return sat, var
    finally:
        while True:
            try:
                os.close(fd)
            except:
                pass
            try:
                os.remove(filename)
                break
            except PermissionError as e:
                print(e)
                time.sleep(1)

def feasible(maxVal, bases):
    t, u = solve(maxVal, bases)
    print("\t", maxVal, t)
    v = None
    assert t in ['SATISFIABLE', 'UNSATISFIABLE'], t
    if (t == 'SATISFIABLE'):
        v = functools.reduce(lambda a,b: a*2+b, reversed(u[0]))
    return (t == 'SATISFIABLE'), (v,u)

def binsearch(func, minVal, maxVal, minData=None, maxData=None, check=True):
    if check:
        isLow, minData = func(minVal)
        isHigh, maxData = func(maxVal)
    else:
        isLow = (minData != None)
        isHigh = (maxData != None)
    assert not isLow
    assert isHigh
    if isHigh:
        sol = maxData
        solVal = maxVal
    midVal = minVal + (maxVal - minVal) // 2
    while (minVal < midVal) and (midVal < maxVal):
        f, v = func(midVal, bases)
        if not f:
            minVal = midVal + 1
        else:
            solVal = maxVal
            maxVal = midVal - 1
            sol = v
        midVal = minVal + (maxVal - minVal) // 2
    return sol, solVal

def brute(bases, start=8192):
    maxVal = 2
    minVal = 1
    sol = None
    solVal = None
    toInc = 1
    while minVal < start:
        minVal = maxVal
        maxVal  += toInc
        toInc = toInc * 2 + 1
    print("\t", minVal, maxVal, toInc)
    while True:
        f, v = feasible(maxVal, bases)
        if not f:
            minVal = maxVal
            maxVal  += toInc
            toInc = toInc * 2 + 1
        else:
            sol = v
            solVal = maxVal
            break
    return binsearch(feasible, minVal, solVal, None, sol, check=False)

for x in range(4, 6+2):
    bases = list(range(2, x))
    print("Solving", bases)
    val = brute(bases, [1, 8100][x==7])[0][0]
    print("Solved", bases, ":", val)