Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment