Skip to content

Instantly share code, notes, and snippets.

@Parcly-Taxel

Parcly-Taxel/zarankiewicz.py

Last active January 4, 2022 05:57
Show Gist options
  • Save Parcly-Taxel/705747d9b62b29967647eb680ca4cdd4 to your computer and use it in GitHub Desktop.
Save Parcly-Taxel/705747d9b62b29967647eb680ca4cdd4 to your computer and use it in GitHub Desktop.
Download ZIP
Zarankiewicz's problem for K_{3,3} through SAT solving (A350237)
Raw
zarankiewicz.py
#!/usr/bin/env python3
from itertools import combinations
from subprocess import run
import numpy as np
import re
lit_re = re.compile(r"-?\d+")
class zaran_cnf:
def __init__(self, mn, ab, pawns):
self.clauses = []
self.pawns = pawns
self.m = m = mn if type(mn) == int else mn[0]
self.n = n = mn if type(mn) == int else mn[1]
self.a = a = ab if type(ab) == int else ab[0]
self.b = b = ab if type(ab) == int else ab[1]
self.bitfield = bitfield = np.arange(m*n).reshape((m,n)) + 1
for rows in combinations(range(m), a):
for cols in combinations(range(n), b):
self.clauses.append(bitfield[np.ix_(rows, cols)].flatten())
self.cursor = m*n+1
def add_card_constraint(self, bits, k, comp=0):
"""Add clauses requiring exactly (comp = 0), at least (1) or at most (-1)
k of the literals in bits to be true, where the variables should all refer
to this class's bitfield."""
cursor = self.cursor
n = len(bits)
res = []
for n0 in range(n-k+1):
for n1 in range(k+1):
b = bits[n0+n1-1]
n_k = cursor + (k+1)*n0 + n1
n1_k = cursor + (k+1)*(n0-1) + n1
n1_k1 = cursor + (k+1)*n0 + n1-1
if n0 == n1 == 0:
res.append([cursor])
elif n0 == 0:
res.extend([[b, -n_k], [-b, -n1_k1, n_k], [-b, n1_k1, -n_k]])
elif n1 == 0:
res.extend([[b, -n1_k, n_k], [b, n1_k, -n_k], [-b, -n_k]])
else:
res.extend([[b, -n1_k, n_k], [b, n1_k, -n_k], [-b, -n1_k1, n_k], [-b, n1_k1, -n_k]])
if comp == 0:
res.append([cursor + (n-k)*(k+1) + k])
elif comp == 1:
res.append([cursor + n0*(k+1) + k for n0 in range(n-k+1)])
elif comp == -1:
res.append([cursor + (n-k)*(k+1) + n1 for n1 in range(k+1)])
self.clauses.extend(res)
self.cursor += (n-k+1)*(k+1)
def add_comparator(self, less_b, greater_b):
"""Add clauses expressing that the (MSB-first) number whose bits are
given by less_b is less than or equal to the number given by greater_b."""
n = len(less_b)
res = []
for i in range(n):
lbi = less_b[i]
gbi = greater_b[i]
part = [[gbi, -lbi], [gbi, lbi], [-gbi, -lbi], [-gbi, lbi]]
pci = self.cursor + i-1
nci = self.cursor + i
if 0 < i < n-1:
res.append([-pci, nci])
if i > 0:
for cl in part:
cl.append(pci)
if i < n-1:
part[1].append(-nci)
part[2].append(-nci)
part[3].append(nci)
else:
part = part[:1]
res.extend(part)
self.clauses.extend(res)
self.cursor += n-1
def set_global_count(self):
self.add_card_constraint(self.bitfield.flatten(), self.pawns)
def set_row_counts(self, counts, floor=0, count_rem=True):
rest_pawns = self.pawns
rest_vars = []
for (i, count) in enumerate(counts):
row = self.bitfield[i]
if count >= 0:
self.add_card_constraint(row, count)
rest_pawns -= count
else:
if floor > 0:
self.add_card_constraint(row, floor, 1)
rest_vars.extend(row)
if count_rem and rest_vars:
self.add_card_constraint(rest_vars, rest_pawns)
for i in range(self.m-1):
if counts[i] == counts[i+1]:
self.add_comparator(self.bitfield[i], self.bitfield[i+1])
def set_col_counts(self, counts, floor=0, count_rem=False):
rest_pawns = self.pawns
rest_vars = []
for (i, count) in enumerate(counts):
col = self.bitfield[:,i]
if count >= 0:
self.add_card_constraint(col, count)
rest_pawns -= count
else:
if floor > 0:
self.add_card_constraint(col, floor, 1)
rest_vars.extend(col)
if count_rem and rest_vars:
self.add_card_constraint(rest_vars, rest_pawns)
for i in range(self.n-1):
if counts[i] == counts[i+1]:
self.add_comparator(self.bitfield[:,i], self.bitfield[:,i+1])
def write(self, cnfn):
nvars = max(abs(l) for cl in self.clauses for l in cl)
nclauses = len(self.clauses)
with open(cnfn, 'w') as f:
print(f"p cnf {nvars} {nclauses}", file=f)
for cl in self.clauses:
print(" ".join(map(str, cl)), "0", file=f)
def solve(cnfn, solver_path, orient=0, proof=None):
cline = [solver_path, "-q", cnfn]
if orient > 0:
cline.append("--sat")
if orient < 0:
cline.append("--unsat")
if proof != None:
cline.append(proof)
proc = run(cline, capture_output=True, encoding="utf-8")
if proc.returncode != 10:
return None # unsatisfiable
return list(map(int, lit_re.findall(proc.stdout)[:-1]))
def add_solution(self, sol):
solbase = sol[:self.m*self.n]
self.clauses.append([-x for x in solbase])
return np.array([int(l > 0) for l in solbase]).reshape(self.m,self.n)
def findallsols(self, cnfn, expected_sols=0, solver_path="./kissat", proof=None):
found_sols = []
while True:
self.write(cnfn)
res = zaran_cnf.solve(cnfn, solver_path, 1 if len(found_sols) < expected_sols else -1, proof)
if res == None:
return found_sols
A = self.add_solution(res)
print(A)
found_sols.append(A)
Raw
zarankiewiczcases.py
#!/usr/bin/env python3
from zarankiewicz import zaran_cnf
# For the generated CNFs and DRAT proofs see
# https://drive.google.com/file/d/1OKXmHd9izhe2BkKTjwy0599OL1pDRSVt/view?usp=sharing
def assert_sols(n, pawns, nsols, rcounts=None, rfloor=0, cfloor=0, ccounts=None, suffix="",
count_global=False, count_rem_row=True, count_rem_col=False):
body = f"{n}_{pawns}{suffix}"
cnf = zaran_cnf(n, 3, pawns)
if count_global:
cnf.set_global_count()
cnf.set_row_counts([-1] * n if rcounts == None else rcounts, rfloor, count_rem_row)
cnf.set_col_counts([-1] * n if ccounts == None else ccounts, cfloor, count_rem_col)
assert len(cnf.findallsols(f"{body}.cnf", nsols, proof=f"{body}.drat")) == nsols
# a(1) = 0, a(2) = 0, a(3) = 1 are trivial
# a(4) = 3
assert_sols(4, 2, 0)
assert_sols(4, 3, 1)
# a(5) = 5
assert_sols(5, 4, 0)
assert_sols(5, 5, 1)
# a(6) = 10
assert_sols(6, 9, 0)
assert_sols(6, 10, 10)
# a(7) = 16
assert_sols(7, 15, 0)
assert_sols(7, 16, 55)
# a(8) = 22
assert_sols(8, 21, 0)
assert_sols(8, 22, 5)
# a(9) = 32
assert_sols(9, 31, 0)
assert_sols(9, 32, 0, [0] + [-1]*8, suffix="_0")
assert_sols(9, 32, 0, [1] + [-1]*8, 1, 1, suffix="_1")
assert_sols(9, 32, 104, [2] + [-1]*8, 2, 2, suffix="_2")
assert_sols(9, 32, 14, [3]*4 + [-1]*5, 3, 3, [3]*4 + [-1]*5, suffix="_3")
# a(10) = 40
assert_sols(10, 39, 0)
assert_sols(10, 40, 0, [0] + [-1]*9, suffix="_0")
assert_sols(10, 40, 0, [1] + [-1]*9, 1, 1, suffix="_1")
assert_sols(10, 40, 0, [2] + [-1]*9, 2, 2, suffix="_2")
assert_sols(10, 40, 0, [3] + [-1]*9, 3, 3, suffix="_3")
assert_sols(10, 40, 16, [4]*10, ccounts=[4]*10, suffix="_4")
# a(11) = 52
assert_sols(11, 51, 0, [0] + [-1]*10, suffix="_0")
assert_sols(11, 51, 0, [1] + [-1]*10, 1, 1, suffix="_1")
assert_sols(11, 51, 0, [2] + [-1]*10, 2, 2, suffix="_2")
assert_sols(11, 51, 0, [3] + [-1]*10, 3, 3, suffix="_3")
assert_sols(11, 51, 0, [4]*4 + [-1]*7, 4, 4, [4]*4 + [-1]*7, suffix="_4")
assert_sols(11, 52, 0, [0] + [-1]*10, suffix="_0")
assert_sols(11, 52, 0, [1] + [-1]*10, 1, 1, suffix="_1")
assert_sols(11, 52, 0, [2] + [-1]*10, 2, 2, suffix="_2")
assert_sols(11, 52, 0, [3] + [-1]*10, 3, 3, suffix="_3")
assert_sols(11, 52, 0, [4]*3 + [5]*8, 4, 4, [4]*3 + [-1]*8, suffix="_4x3")
assert_sols(11, 52, 3, [4]*4 + [-1]*7, 4, 4, [4]*4 + [-1]*7, suffix="_4x4+")
# a(12) = 64
assert_sols(12, 63, 0, [0] + [-1]*11, suffix="_0")
assert_sols(12, 63, 0, [1] + [-1]*11, 1, 1, suffix="_1")
assert_sols(12, 63, 0, [2] + [-1]*11, 2, 2, suffix="_2")
assert_sols(12, 63, 0, [3] + [-1]*11, 3, 3, suffix="_3")
assert_sols(12, 63, 0, [4]*2 + [-1]*10, 4, 4, suffix="_4x2")
assert_sols(12, 63, 0, [4]*1 + [5]*7 + [-1]*4, 5, 4, suffix="_4x1")
assert_sols(12, 63, 0, [5]*9 + [-1]*3, 5, 5, [5]*9 + [-1]*3, suffix="_5")
assert_sols(12, 64, 0, [0] + [-1]*11, suffix="_0")
assert_sols(12, 64, 0, [1] + [-1]*11, 1, 1, suffix="_1")
assert_sols(12, 64, 0, [2] + [-1]*11, 2, 2, suffix="_2")
assert_sols(12, 64, 0, [3] + [-1]*11, 3, 3, suffix="_3")
assert_sols(12, 64, 0, [4]*2 + [-1]*10, 4, 4, suffix="_4x2")
assert_sols(12, 64, 1, [4]*1 + [5]*6 + [-1]*5, 5, 5, [4]*1 + [5]*6 + [-1]*5, suffix="_4x1_4x1")
assert_sols(12, 64, 1, [5]*8 + [-1]*4, 5, 5, [5]*8 + [-1]*4, suffix="_4x0_4x0")
assert_sols(12, 64, 0, [4]*1 + [5]*6 + [-1]*5, 5, 5, [5]*8 + [-1]*4, suffix="_4x1_4x0")
# a(13) = 77
assert_sols(13, 76, 0, [0] + [-1]*12, suffix="_0")
assert_sols(13, 76, 0, [1] + [-1]*12, 1, 1, suffix="_1")
assert_sols(13, 76, 0, [2] + [-1]*12, 2, 2, suffix="_2")
assert_sols(13, 76, 0, [3] + [-1]*12, 3, 3, suffix="_3")
assert_sols(13, 76, 0, [4]*2 + [-1]*11, 4, 4, suffix="_4x2")
assert_sols(13, 76, 0, [4, 5] + [-1]*11, 5, 4, suffix="_4_5")
assert_sols(13, 76, 0, [4] + [6]*12, 6, 4, suffix="_4_6")
assert_sols(13, 76, 0, [5]*3 + [-1]*10, 5, 5, [5]*2 + [-1]*11, suffix="_5x3")
assert_sols(13, 76, 0, [5]*2 + [6]*11, ccounts=[5]*2 + [6]*11, suffix="_5x2")
assert_sols(13, 77, 0, [0] + [-1]*12, suffix="_0")
assert_sols(13, 77, 0, [1] + [-1]*12, 1, 1, suffix="_1")
assert_sols(13, 77, 0, [2] + [-1]*12, 2, 2, suffix="_2")
assert_sols(13, 77, 0, [3] + [-1]*12, 3, 3, suffix="_3")
assert_sols(13, 77, 0, [4]*2 + [-1]*11, 4, 4, suffix="_4x2")
assert_sols(13, 77, 0, [4, 5] + [-1]*11, 5, 4, suffix="_4_5")
assert_sols(13, 77, 0, [4] + [6]*11 + [7], 6, 4, suffix="_4_6")
assert_sols(13, 77, 0, [5]*4 + [-1]*9, 5, 5, [5] + [-1]*12, suffix="_5x4")
assert_sols(13, 77, 0, [5] + [6]*12, 5, 5, [5] + [6]*8 + [-1]*4, suffix="_5_6x12")
assert_sols(13, 77, 0, [5]*2 + [6]*10 + [7], 5, 5, [5]*2 + [6]*8 + [-1]*3, suffix="_5x2_6x10")
assert_sols(13, 77, 1, [5]*3 + [6]*8 + [-1]*2, 6, 6, [5]*3 + [6]*8 + [-1]*2, suffix="_5x3_6x8")
Raw
zarankiewiczcases14.py
#!/usr/bin/env python3
from math import comb
from zarankiewicz import zaran_cnf
# https://drive.google.com/file/d/10IZiAijEgnq9J01gW__fq7t2403dOGcM/view?usp=sharing
def assert_sols(n, pawns, nsols, rcounts=None, rfloor=0, cfloor=0, ccounts=None, suffix="",
count_global=False, count_rem_row=True, count_rem_col=False):
body = f"{n}_{pawns}{suffix}"
cnf = zaran_cnf(n, 3, pawns)
if count_global:
cnf.set_global_count()
cnf.set_row_counts([-1] * n if rcounts == None else rcounts, rfloor, count_rem_row)
cnf.set_col_counts([-1] * n if ccounts == None else ccounts, cfloor, count_rem_col)
assert len(cnf.findallsols(f"{body}.cnf", nsols, proof=f"{body}.drat")) == nsols
# 137 admissible pawn count sequences for the 14/90 pawns (14/106 edges) case
# from arguments A and D of Guy's paper https://oeis.org/A001197/a001197.pdf
# forpart(v=106, if(sum(i=1, 14, binomial(v[i],3)) <= (3-1)*binomial(14,3), print(vector(14, i, 14-v[15-i]),"," )), [0,10], 14)
# (the D-exclusions can only be made once all A-admissible sequences are obtained;
# they consist of all 14 sequences with an 11-row (3 pawns))
pawnseqs = [[6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 12],
[5, 5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 8, 11],
[5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 8, 11],
[5, 5, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 11],
[5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 11],
[6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 11],
[5, 5, 5, 6, 6, 6, 6, 6, 6, 6, 7, 7, 9, 10],
[5, 5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 9, 10],
[5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 9, 10],
[5, 5, 5, 6, 6, 6, 6, 6, 6, 6, 7, 8, 8, 10],
[4, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 8, 8, 10],
[5, 5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 8, 8, 10],
[5, 5, 5, 5, 6, 6, 6, 6, 7, 7, 7, 7, 8, 10],
[4, 5, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 8, 10],
[5, 5, 5, 6, 6, 6, 6, 6, 6, 7, 7, 7, 8, 10],
[4, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 8, 10],
[5, 5, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 8, 10],
[5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 8, 10],
[6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 8, 10],
[5, 5, 5, 5, 5, 6, 7, 7, 7, 7, 7, 7, 7, 10],
[4, 5, 5, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 10],
[5, 5, 5, 5, 6, 6, 6, 7, 7, 7, 7, 7, 7, 10],
[4, 5, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 10],
[5, 5, 5, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 10],
[4, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 10],
[5, 5, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 10],
[5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 10],
[6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 10],
[5, 5, 5, 5, 6, 6, 6, 6, 6, 7, 7, 8, 9, 9],
[4, 5, 6, 6, 6, 6, 6, 6, 6, 6, 7, 8, 9, 9],
[5, 5, 5, 6, 6, 6, 6, 6, 6, 6, 7, 8, 9, 9],
[4, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 8, 9, 9],
[5, 5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 8, 9, 9],
[5, 5, 5, 5, 5, 6, 6, 7, 7, 7, 7, 7, 9, 9],
[4, 5, 5, 6, 6, 6, 6, 6, 7, 7, 7, 7, 9, 9],
[5, 5, 5, 5, 6, 6, 6, 6, 7, 7, 7, 7, 9, 9],
[4, 5, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 9, 9],
[5, 5, 5, 6, 6, 6, 6, 6, 6, 7, 7, 7, 9, 9],
[4, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 9, 9],
[5, 5, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 9, 9],
[5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 9, 9],
[6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 9, 9],
[5, 5, 5, 5, 5, 6, 6, 6, 7, 7, 8, 8, 8, 9],
[5, 5, 5, 5, 6, 6, 6, 6, 6, 7, 8, 8, 8, 9],
[4, 5, 6, 6, 6, 6, 6, 6, 6, 6, 8, 8, 8, 9],
[5, 5, 5, 6, 6, 6, 6, 6, 6, 6, 8, 8, 8, 9],
[5, 5, 5, 5, 5, 6, 6, 7, 7, 7, 7, 8, 8, 9],
[4, 5, 5, 6, 6, 6, 6, 6, 7, 7, 7, 8, 8, 9],
[5, 5, 5, 5, 6, 6, 6, 6, 7, 7, 7, 8, 8, 9],
[4, 5, 6, 6, 6, 6, 6, 6, 6, 7, 7, 8, 8, 9],
[5, 5, 5, 6, 6, 6, 6, 6, 6, 7, 7, 8, 8, 9],
[4, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 8, 8, 9],
[5, 5, 6, 6, 6, 6, 6, 6, 6, 6, 7, 8, 8, 9],
[5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 8, 8, 9],
[4, 5, 5, 5, 6, 6, 7, 7, 7, 7, 7, 7, 8, 9],
[5, 5, 5, 5, 5, 6, 7, 7, 7, 7, 7, 7, 8, 9],
[4, 4, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 8, 9],
[4, 5, 5, 6, 6, 6, 6, 7, 7, 7, 7, 7, 8, 9],
[5, 5, 5, 5, 6, 6, 6, 7, 7, 7, 7, 7, 8, 9],
[3, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 8, 9],
[4, 5, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 8, 9],
[5, 5, 5, 6, 6, 6, 6, 6, 7, 7, 7, 7, 8, 9],
[4, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 8, 9],
[5, 5, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 8, 9],
[5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 8, 9],
[6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 8, 9],
[4, 4, 5, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 9],
[4, 5, 5, 5, 6, 7, 7, 7, 7, 7, 7, 7, 7, 9],
[5, 5, 5, 5, 5, 7, 7, 7, 7, 7, 7, 7, 7, 9],
[3, 5, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 9],
[4, 4, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 9],
[4, 5, 5, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 9],
[5, 5, 5, 5, 6, 6, 7, 7, 7, 7, 7, 7, 7, 9],
[3, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 9],
[4, 5, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 9],
[5, 5, 5, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 9],
[4, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 9],
[5, 5, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 9],
[5, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 9],
[6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 9],
[5, 5, 5, 5, 5, 6, 6, 6, 7, 8, 8, 8, 8, 8],
[4, 5, 5, 6, 6, 6, 6, 6, 6, 8, 8, 8, 8, 8],
[5, 5, 5, 5, 6, 6, 6, 6, 6, 8, 8, 8, 8, 8],
[5, 5, 5, 5, 5, 5, 7, 7, 7, 7, 8, 8, 8, 8],
[4, 5, 5, 5, 6, 6, 6, 7, 7, 7, 8, 8, 8, 8],
[5, 5, 5, 5, 5, 6, 6, 7, 7, 7, 8, 8, 8, 8],
[4, 4, 6, 6, 6, 6, 6, 6, 7, 7, 8, 8, 8, 8],
[4, 5, 5, 6, 6, 6, 6, 6, 7, 7, 8, 8, 8, 8],
[5, 5, 5, 5, 6, 6, 6, 6, 7, 7, 8, 8, 8, 8],
[3, 6, 6, 6, 6, 6, 6, 6, 6, 7, 8, 8, 8, 8],
[4, 5, 6, 6, 6, 6, 6, 6, 6, 7, 8, 8, 8, 8],
[5, 5, 5, 6, 6, 6, 6, 6, 6, 7, 8, 8, 8, 8],
[4, 6, 6, 6, 6, 6, 6, 6, 6, 6, 8, 8, 8, 8],
[5, 5, 6, 6, 6, 6, 6, 6, 6, 6, 8, 8, 8, 8],
[4, 5, 5, 5, 5, 7, 7, 7, 7, 7, 7, 8, 8, 8],
[4, 4, 5, 6, 6, 6, 7, 7, 7, 7, 7, 8, 8, 8],
[4, 5, 5, 5, 6, 6, 7, 7, 7, 7, 7, 8, 8, 8],
[5, 5, 5, 5, 5, 6, 7, 7, 7, 7, 7, 8, 8, 8],
[4, 4, 6, 6, 6, 6, 6, 7, 7, 7, 7, 8, 8, 8],
[4, 5, 5, 6, 6, 6, 6, 7, 7, 7, 7, 8, 8, 8],
[5, 5, 5, 5, 6, 6, 6, 7, 7, 7, 7, 8, 8, 8],
[3, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 8, 8, 8],
[4, 5, 6, 6, 6, 6, 6, 6, 7, 7, 7, 8, 8, 8],
[5, 5, 5, 6, 6, 6, 6, 6, 7, 7, 7, 8, 8, 8],
[4, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 8, 8, 8],
[5, 5, 6, 6, 6, 6, 6, 6, 6, 7, 7, 8, 8, 8],
[5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 8, 8, 8],
[6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 8, 8, 8],
[4, 4, 5, 5, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8],
[4, 4, 5, 6, 6, 7, 7, 7, 7, 7, 7, 7, 8, 8],
[4, 5, 5, 5, 6, 7, 7, 7, 7, 7, 7, 7, 8, 8],
[5, 5, 5, 5, 5, 7, 7, 7, 7, 7, 7, 7, 8, 8],
[3, 5, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 8, 8],
[4, 4, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 8, 8],
[4, 5, 5, 6, 6, 6, 7, 7, 7, 7, 7, 7, 8, 8],
[5, 5, 5, 5, 6, 6, 7, 7, 7, 7, 7, 7, 8, 8],
[3, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 8, 8],
[4, 5, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 8, 8],
[5, 5, 5, 6, 6, 6, 6, 7, 7, 7, 7, 7, 8, 8],
[4, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 8, 8],
[5, 5, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 8, 8],
[5, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 8, 8],
[6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 8, 8],
[3, 5, 5, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8],
[4, 4, 5, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8],
[4, 5, 5, 5, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8],
[3, 5, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 8],
[4, 4, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 8],
[4, 5, 5, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 8],
[5, 5, 5, 5, 6, 7, 7, 7, 7, 7, 7, 7, 7, 8],
[3, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 8],
[4, 5, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 8],
[5, 5, 5, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 8],
[4, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 8],
[5, 5, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 8],
[5, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 8],
[6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 8],
[3, 4, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7],
[3, 5, 5, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7],
[4, 4, 5, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7],
[3, 5, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7],
[4, 4, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7],
[4, 5, 5, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7],
[5, 5, 5, 5, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7],
[3, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7],
[4, 5, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7],
[5, 5, 5, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7],
[4, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7],
[5, 5, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7],
[5, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7],
[6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7]]
assert_sols(14, 90, 0, [4,4,7,7] + [-1]*10, 4, 4, suffix="_4477")
assert_sols(14, 90, 0, [4,5,7,7] + [-1]*10, 4, 4, suffix="_4577")
assert_sols(14, 90, 0, [4] + [6]*5 + [-1]*8, 4, 4, suffix="_4_6x5")
assert_sols(14, 90, 0, [5,5,6,6] + [-1]*10, 5, 5, suffix="_5566")
assert_sols(14, 90, 0, [5]*4 + [7]*4 + [-1]*6, 5, 5, suffix="_5x4_7x4")
assert_sols(14, 90, 0, [6]*6 + [-1]*8, 5, 5, suffix="_6x6")
def is_seq_excluded(seq, counts):
return all(seq.count(c) >= m for (c, m) in counts)
for ds in pawnseqs:
if sum(comb(c-1, 2) for c in [14-x for x in ds[::-1]][:11]) <= 2*comb(13,2):
print(ds)
# the lack of any output here (conducted in the extremal graph setting, not the pawns one)
# justifies excluding all sequences with an 11-row (3 pawns)
if all(not is_seq_excluded(ds, counts) for counts in [((3,1),), ((4,2),(7,2)), ((4,1),(5,1),(7,2)), ((4,1),(6,5)), ((5,2),(6,2)), ((5,4),(7,4)), ((6,6),)]):
print("->", ds)
# 327 admissible pawn count sequences for the 14/91 pawns (14/105 edges) case
pawnseqs2 = [[6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 13],
[5, 5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 8, 12],
[5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 8, 12],
[5, 5, 5, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 12],
[5, 5, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 12],
[5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 12],
[6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 12],
[5, 5, 5, 6, 6, 6, 6, 6, 6, 6, 7, 7, 9, 11],
[4, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 9, 11],
[5, 5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 9, 11],
[5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 9, 11],
[5, 5, 5, 5, 6, 6, 6, 6, 6, 7, 7, 8, 8, 11],
[4, 5, 6, 6, 6, 6, 6, 6, 6, 6, 7, 8, 8, 11],
[5, 5, 5, 6, 6, 6, 6, 6, 6, 6, 7, 8, 8, 11],
[4, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 8, 8, 11],
[5, 5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 8, 8, 11],
[5, 5, 5, 5, 5, 6, 6, 7, 7, 7, 7, 7, 8, 11],
[5, 5, 5, 5, 6, 6, 6, 6, 7, 7, 7, 7, 8, 11],
[4, 5, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 8, 11],
[5, 5, 5, 6, 6, 6, 6, 6, 6, 7, 7, 7, 8, 11],
[4, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 8, 11],
[5, 5, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 8, 11],
[5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 8, 11],
[6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 8, 11],
[5, 5, 5, 5, 5, 6, 7, 7, 7, 7, 7, 7, 7, 11],
[4, 5, 5, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 11],
[5, 5, 5, 5, 6, 6, 6, 7, 7, 7, 7, 7, 7, 11],
[4, 5, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 11],
[5, 5, 5, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 11],
[4, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 11],
[5, 5, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 11],
[5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 11],
[6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 11],
[5, 5, 5, 6, 6, 6, 6, 6, 6, 6, 6, 8, 10, 10],
[5, 5, 5, 6, 6, 6, 6, 6, 6, 6, 7, 7, 10, 10],
[4, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 10, 10],
[5, 5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 10, 10],
[5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 10, 10],
[5, 5, 5, 6, 6, 6, 6, 6, 6, 6, 6, 9, 9, 10],
[5, 5, 5, 5, 6, 6, 6, 6, 6, 6, 8, 8, 9, 10],
[5, 5, 5, 5, 5, 6, 6, 6, 7, 7, 7, 8, 9, 10],
[4, 5, 5, 6, 6, 6, 6, 6, 6, 7, 7, 8, 9, 10],
[5, 5, 5, 5, 6, 6, 6, 6, 6, 7, 7, 8, 9, 10],
[4, 5, 6, 6, 6, 6, 6, 6, 6, 6, 7, 8, 9, 10],
[5, 5, 5, 6, 6, 6, 6, 6, 6, 6, 7, 8, 9, 10],
[4, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 8, 9, 10],
[5, 5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 8, 9, 10],
[5, 5, 5, 5, 5, 5, 7, 7, 7, 7, 7, 7, 9, 10],
[5, 5, 5, 5, 5, 6, 6, 7, 7, 7, 7, 7, 9, 10],
[4, 5, 5, 6, 6, 6, 6, 6, 7, 7, 7, 7, 9, 10],
[5, 5, 5, 5, 6, 6, 6, 6, 7, 7, 7, 7, 9, 10],
[4, 5, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 9, 10],
[5, 5, 5, 6, 6, 6, 6, 6, 6, 7, 7, 7, 9, 10],
[4, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 9, 10],
[5, 5, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 9, 10],
[5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 9, 10],
[6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 9, 10],
[5, 5, 5, 5, 5, 6, 6, 6, 6, 8, 8, 8, 8, 10],
[5, 5, 5, 5, 5, 6, 6, 6, 7, 7, 8, 8, 8, 10],
[4, 5, 5, 6, 6, 6, 6, 6, 6, 7, 8, 8, 8, 10],
[5, 5, 5, 5, 6, 6, 6, 6, 6, 7, 8, 8, 8, 10],
[4, 5, 6, 6, 6, 6, 6, 6, 6, 6, 8, 8, 8, 10],
[5, 5, 5, 6, 6, 6, 6, 6, 6, 6, 8, 8, 8, 10],
[5, 5, 5, 5, 5, 5, 7, 7, 7, 7, 7, 8, 8, 10],
[4, 5, 5, 5, 6, 6, 6, 7, 7, 7, 7, 8, 8, 10],
[5, 5, 5, 5, 5, 6, 6, 7, 7, 7, 7, 8, 8, 10],
[4, 4, 6, 6, 6, 6, 6, 6, 7, 7, 7, 8, 8, 10],
[4, 5, 5, 6, 6, 6, 6, 6, 7, 7, 7, 8, 8, 10],
[5, 5, 5, 5, 6, 6, 6, 6, 7, 7, 7, 8, 8, 10],
[3, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 8, 8, 10],
[4, 5, 6, 6, 6, 6, 6, 6, 6, 7, 7, 8, 8, 10],
[5, 5, 5, 6, 6, 6, 6, 6, 6, 7, 7, 8, 8, 10],
[4, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 8, 8, 10],
[5, 5, 6, 6, 6, 6, 6, 6, 6, 6, 7, 8, 8, 10],
[5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 8, 8, 10],
[4, 5, 5, 5, 5, 7, 7, 7, 7, 7, 7, 7, 8, 10],
[4, 4, 5, 6, 6, 6, 7, 7, 7, 7, 7, 7, 8, 10],
[4, 5, 5, 5, 6, 6, 7, 7, 7, 7, 7, 7, 8, 10],
[5, 5, 5, 5, 5, 6, 7, 7, 7, 7, 7, 7, 8, 10],
[3, 5, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 8, 10],
[4, 4, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 8, 10],
[4, 5, 5, 6, 6, 6, 6, 7, 7, 7, 7, 7, 8, 10],
[5, 5, 5, 5, 6, 6, 6, 7, 7, 7, 7, 7, 8, 10],
[3, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 8, 10],
[4, 5, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 8, 10],
[5, 5, 5, 6, 6, 6, 6, 6, 7, 7, 7, 7, 8, 10],
[4, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 8, 10],
[5, 5, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 8, 10],
[5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 8, 10],
[6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 8, 10],
[4, 4, 5, 5, 7, 7, 7, 7, 7, 7, 7, 7, 7, 10],
[4, 4, 5, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 10],
[4, 5, 5, 5, 6, 7, 7, 7, 7, 7, 7, 7, 7, 10],
[5, 5, 5, 5, 5, 7, 7, 7, 7, 7, 7, 7, 7, 10],
[3, 5, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 10],
[4, 4, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 10],
[4, 5, 5, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 10],
[5, 5, 5, 5, 6, 6, 7, 7, 7, 7, 7, 7, 7, 10],
[3, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 10],
[4, 5, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 10],
[5, 5, 5, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 10],
[4, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 10],
[5, 5, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 10],
[5, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 10],
[6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 10],
[5, 5, 5, 5, 6, 6, 6, 6, 6, 6, 8, 9, 9, 9],
[5, 5, 5, 5, 5, 6, 6, 6, 7, 7, 7, 9, 9, 9],
[4, 5, 5, 6, 6, 6, 6, 6, 6, 7, 7, 9, 9, 9],
[5, 5, 5, 5, 6, 6, 6, 6, 6, 7, 7, 9, 9, 9],
[4, 5, 6, 6, 6, 6, 6, 6, 6, 6, 7, 9, 9, 9],
[5, 5, 5, 6, 6, 6, 6, 6, 6, 6, 7, 9, 9, 9],
[4, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 9, 9, 9],
[5, 5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 9, 9, 9],
[5, 5, 5, 5, 5, 6, 6, 6, 6, 8, 8, 8, 9, 9],
[5, 5, 5, 5, 5, 5, 6, 7, 7, 7, 8, 8, 9, 9],
[4, 5, 5, 5, 6, 6, 6, 6, 7, 7, 8, 8, 9, 9],
[5, 5, 5, 5, 5, 6, 6, 6, 7, 7, 8, 8, 9, 9],
[4, 4, 6, 6, 6, 6, 6, 6, 6, 7, 8, 8, 9, 9],
[4, 5, 5, 6, 6, 6, 6, 6, 6, 7, 8, 8, 9, 9],
[5, 5, 5, 5, 6, 6, 6, 6, 6, 7, 8, 8, 9, 9],
[4, 5, 6, 6, 6, 6, 6, 6, 6, 6, 8, 8, 9, 9],
[5, 5, 5, 6, 6, 6, 6, 6, 6, 6, 8, 8, 9, 9],
[4, 5, 5, 5, 5, 6, 7, 7, 7, 7, 7, 8, 9, 9],
[5, 5, 5, 5, 5, 5, 7, 7, 7, 7, 7, 8, 9, 9],
[4, 4, 5, 6, 6, 6, 6, 7, 7, 7, 7, 8, 9, 9],
[4, 5, 5, 5, 6, 6, 6, 7, 7, 7, 7, 8, 9, 9],
[5, 5, 5, 5, 5, 6, 6, 7, 7, 7, 7, 8, 9, 9],
[4, 4, 6, 6, 6, 6, 6, 6, 7, 7, 7, 8, 9, 9],
[4, 5, 5, 6, 6, 6, 6, 6, 7, 7, 7, 8, 9, 9],
[5, 5, 5, 5, 6, 6, 6, 6, 7, 7, 7, 8, 9, 9],
[3, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 8, 9, 9],
[4, 5, 6, 6, 6, 6, 6, 6, 6, 7, 7, 8, 9, 9],
[5, 5, 5, 6, 6, 6, 6, 6, 6, 7, 7, 8, 9, 9],
[4, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 8, 9, 9],
[5, 5, 6, 6, 6, 6, 6, 6, 6, 6, 7, 8, 9, 9],
[5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 8, 9, 9],
[4, 5, 5, 5, 5, 7, 7, 7, 7, 7, 7, 7, 9, 9],
[4, 4, 5, 6, 6, 6, 7, 7, 7, 7, 7, 7, 9, 9],
[4, 5, 5, 5, 6, 6, 7, 7, 7, 7, 7, 7, 9, 9],
[5, 5, 5, 5, 5, 6, 7, 7, 7, 7, 7, 7, 9, 9],
[3, 5, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 9, 9],
[4, 4, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 9, 9],
[4, 5, 5, 6, 6, 6, 6, 7, 7, 7, 7, 7, 9, 9],
[5, 5, 5, 5, 6, 6, 6, 7, 7, 7, 7, 7, 9, 9],
[3, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 9, 9],
[4, 5, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 9, 9],
[5, 5, 5, 6, 6, 6, 6, 6, 7, 7, 7, 7, 9, 9],
[4, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 9, 9],
[5, 5, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 9, 9],
[5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 9, 9],
[6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 9, 9],
[5, 5, 5, 5, 5, 5, 6, 6, 8, 8, 8, 8, 8, 9],
[4, 5, 5, 5, 5, 6, 6, 7, 7, 8, 8, 8, 8, 9],
[5, 5, 5, 5, 5, 5, 6, 7, 7, 8, 8, 8, 8, 9],
[4, 5, 5, 5, 6, 6, 6, 6, 7, 8, 8, 8, 8, 9],
[5, 5, 5, 5, 5, 6, 6, 6, 7, 8, 8, 8, 8, 9],
[4, 4, 6, 6, 6, 6, 6, 6, 6, 8, 8, 8, 8, 9],
[4, 5, 5, 6, 6, 6, 6, 6, 6, 8, 8, 8, 8, 9],
[5, 5, 5, 5, 6, 6, 6, 6, 6, 8, 8, 8, 8, 9],
[4, 5, 5, 5, 5, 6, 7, 7, 7, 7, 8, 8, 8, 9],
[5, 5, 5, 5, 5, 5, 7, 7, 7, 7, 8, 8, 8, 9],
[4, 4, 5, 6, 6, 6, 6, 7, 7, 7, 8, 8, 8, 9],
[4, 5, 5, 5, 6, 6, 6, 7, 7, 7, 8, 8, 8, 9],
[5, 5, 5, 5, 5, 6, 6, 7, 7, 7, 8, 8, 8, 9],
[3, 5, 6, 6, 6, 6, 6, 6, 7, 7, 8, 8, 8, 9],
[4, 4, 6, 6, 6, 6, 6, 6, 7, 7, 8, 8, 8, 9],
[4, 5, 5, 6, 6, 6, 6, 6, 7, 7, 8, 8, 8, 9],
[5, 5, 5, 5, 6, 6, 6, 6, 7, 7, 8, 8, 8, 9],
[3, 6, 6, 6, 6, 6, 6, 6, 6, 7, 8, 8, 8, 9],
[4, 5, 6, 6, 6, 6, 6, 6, 6, 7, 8, 8, 8, 9],
[5, 5, 5, 6, 6, 6, 6, 6, 6, 7, 8, 8, 8, 9],
[4, 6, 6, 6, 6, 6, 6, 6, 6, 6, 8, 8, 8, 9],
[5, 5, 6, 6, 6, 6, 6, 6, 6, 6, 8, 8, 8, 9],
[4, 4, 5, 5, 6, 7, 7, 7, 7, 7, 7, 8, 8, 9],
[4, 5, 5, 5, 5, 7, 7, 7, 7, 7, 7, 8, 8, 9],
[3, 5, 5, 6, 6, 6, 7, 7, 7, 7, 7, 8, 8, 9],
[4, 4, 5, 6, 6, 6, 7, 7, 7, 7, 7, 8, 8, 9],
[4, 5, 5, 5, 6, 6, 7, 7, 7, 7, 7, 8, 8, 9],
[5, 5, 5, 5, 5, 6, 7, 7, 7, 7, 7, 8, 8, 9],
[3, 5, 6, 6, 6, 6, 6, 7, 7, 7, 7, 8, 8, 9],
[4, 4, 6, 6, 6, 6, 6, 7, 7, 7, 7, 8, 8, 9],
[4, 5, 5, 6, 6, 6, 6, 7, 7, 7, 7, 8, 8, 9],
[5, 5, 5, 5, 6, 6, 6, 7, 7, 7, 7, 8, 8, 9],
[3, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 8, 8, 9],
[4, 5, 6, 6, 6, 6, 6, 6, 7, 7, 7, 8, 8, 9],
[5, 5, 5, 6, 6, 6, 6, 6, 7, 7, 7, 8, 8, 9],
[4, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 8, 8, 9],
[5, 5, 6, 6, 6, 6, 6, 6, 6, 7, 7, 8, 8, 9],
[5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 8, 8, 9],
[6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 8, 8, 9],
[4, 4, 4, 6, 7, 7, 7, 7, 7, 7, 7, 7, 8, 9],
[3, 5, 5, 5, 7, 7, 7, 7, 7, 7, 7, 7, 8, 9],
[4, 4, 5, 5, 7, 7, 7, 7, 7, 7, 7, 7, 8, 9],
[3, 4, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 8, 9],
[3, 5, 5, 6, 6, 7, 7, 7, 7, 7, 7, 7, 8, 9],
[4, 4, 5, 6, 6, 7, 7, 7, 7, 7, 7, 7, 8, 9],
[4, 5, 5, 5, 6, 7, 7, 7, 7, 7, 7, 7, 8, 9],
[5, 5, 5, 5, 5, 7, 7, 7, 7, 7, 7, 7, 8, 9],
[3, 5, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 8, 9],
[4, 4, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 8, 9],
[4, 5, 5, 6, 6, 6, 7, 7, 7, 7, 7, 7, 8, 9],
[5, 5, 5, 5, 6, 6, 7, 7, 7, 7, 7, 7, 8, 9],
[3, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 8, 9],
[4, 5, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 8, 9],
[5, 5, 5, 6, 6, 6, 6, 7, 7, 7, 7, 7, 8, 9],
[4, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 8, 9],
[5, 5, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 8, 9],
[5, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 8, 9],
[6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 8, 9],
[4, 4, 4, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 9],
[3, 4, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 9],
[3, 5, 5, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 9],
[4, 4, 5, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 9],
[4, 5, 5, 5, 7, 7, 7, 7, 7, 7, 7, 7, 7, 9],
[3, 5, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 9],
[4, 4, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 9],
[4, 5, 5, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 9],
[5, 5, 5, 5, 6, 7, 7, 7, 7, 7, 7, 7, 7, 9],
[3, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 9],
[4, 5, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 9],
[5, 5, 5, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 9],
[4, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 9],
[5, 5, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 9],
[5, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 9],
[6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 9],
[5, 5, 5, 5, 5, 5, 5, 8, 8, 8, 8, 8, 8, 8],
[4, 5, 5, 5, 5, 6, 6, 7, 8, 8, 8, 8, 8, 8],
[5, 5, 5, 5, 5, 5, 6, 7, 8, 8, 8, 8, 8, 8],
[4, 4, 5, 6, 6, 6, 6, 6, 8, 8, 8, 8, 8, 8],
[4, 5, 5, 5, 6, 6, 6, 6, 8, 8, 8, 8, 8, 8],
[5, 5, 5, 5, 5, 6, 6, 6, 8, 8, 8, 8, 8, 8],
[4, 4, 5, 5, 6, 6, 7, 7, 7, 8, 8, 8, 8, 8],
[4, 5, 5, 5, 5, 6, 7, 7, 7, 8, 8, 8, 8, 8],
[5, 5, 5, 5, 5, 5, 7, 7, 7, 8, 8, 8, 8, 8],
[3, 5, 5, 6, 6, 6, 6, 7, 7, 8, 8, 8, 8, 8],
[4, 4, 5, 6, 6, 6, 6, 7, 7, 8, 8, 8, 8, 8],
[4, 5, 5, 5, 6, 6, 6, 7, 7, 8, 8, 8, 8, 8],
[5, 5, 5, 5, 5, 6, 6, 7, 7, 8, 8, 8, 8, 8],
[3, 5, 6, 6, 6, 6, 6, 6, 7, 8, 8, 8, 8, 8],
[4, 4, 6, 6, 6, 6, 6, 6, 7, 8, 8, 8, 8, 8],
[4, 5, 5, 6, 6, 6, 6, 6, 7, 8, 8, 8, 8, 8],
[5, 5, 5, 5, 6, 6, 6, 6, 7, 8, 8, 8, 8, 8],
[3, 6, 6, 6, 6, 6, 6, 6, 6, 8, 8, 8, 8, 8],
[4, 5, 6, 6, 6, 6, 6, 6, 6, 8, 8, 8, 8, 8],
[5, 5, 5, 6, 6, 6, 6, 6, 6, 8, 8, 8, 8, 8],
[4, 4, 4, 6, 6, 7, 7, 7, 7, 7, 8, 8, 8, 8],
[3, 5, 5, 5, 6, 7, 7, 7, 7, 7, 8, 8, 8, 8],
[4, 4, 5, 5, 6, 7, 7, 7, 7, 7, 8, 8, 8, 8],
[4, 5, 5, 5, 5, 7, 7, 7, 7, 7, 8, 8, 8, 8],
[3, 5, 5, 6, 6, 6, 7, 7, 7, 7, 8, 8, 8, 8],
[4, 4, 5, 6, 6, 6, 7, 7, 7, 7, 8, 8, 8, 8],
[4, 5, 5, 5, 6, 6, 7, 7, 7, 7, 8, 8, 8, 8],
[5, 5, 5, 5, 5, 6, 7, 7, 7, 7, 8, 8, 8, 8],
[3, 5, 6, 6, 6, 6, 6, 7, 7, 7, 8, 8, 8, 8],
[4, 4, 6, 6, 6, 6, 6, 7, 7, 7, 8, 8, 8, 8],
[4, 5, 5, 6, 6, 6, 6, 7, 7, 7, 8, 8, 8, 8],
[5, 5, 5, 5, 6, 6, 6, 7, 7, 7, 8, 8, 8, 8],
[3, 6, 6, 6, 6, 6, 6, 6, 7, 7, 8, 8, 8, 8],
[4, 5, 6, 6, 6, 6, 6, 6, 7, 7, 8, 8, 8, 8],
[5, 5, 5, 6, 6, 6, 6, 6, 7, 7, 8, 8, 8, 8],
[4, 6, 6, 6, 6, 6, 6, 6, 6, 7, 8, 8, 8, 8],
[5, 5, 6, 6, 6, 6, 6, 6, 6, 7, 8, 8, 8, 8],
[5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 8, 8, 8, 8],
[4, 4, 4, 6, 7, 7, 7, 7, 7, 7, 7, 8, 8, 8],
[3, 5, 5, 5, 7, 7, 7, 7, 7, 7, 7, 8, 8, 8],
[4, 4, 5, 5, 7, 7, 7, 7, 7, 7, 7, 8, 8, 8],
[3, 4, 6, 6, 6, 7, 7, 7, 7, 7, 7, 8, 8, 8],
[3, 5, 5, 6, 6, 7, 7, 7, 7, 7, 7, 8, 8, 8],
[4, 4, 5, 6, 6, 7, 7, 7, 7, 7, 7, 8, 8, 8],
[4, 5, 5, 5, 6, 7, 7, 7, 7, 7, 7, 8, 8, 8],
[5, 5, 5, 5, 5, 7, 7, 7, 7, 7, 7, 8, 8, 8],
[3, 5, 6, 6, 6, 6, 7, 7, 7, 7, 7, 8, 8, 8],
[4, 4, 6, 6, 6, 6, 7, 7, 7, 7, 7, 8, 8, 8],
[4, 5, 5, 6, 6, 6, 7, 7, 7, 7, 7, 8, 8, 8],
[5, 5, 5, 5, 6, 6, 7, 7, 7, 7, 7, 8, 8, 8],
[3, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 8, 8, 8],
[4, 5, 6, 6, 6, 6, 6, 7, 7, 7, 7, 8, 8, 8],
[5, 5, 5, 6, 6, 6, 6, 7, 7, 7, 7, 8, 8, 8],
[4, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 8, 8, 8],
[5, 5, 6, 6, 6, 6, 6, 6, 7, 7, 7, 8, 8, 8],
[5, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 8, 8, 8],
[6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 8, 8, 8],
[3, 4, 5, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8],
[4, 4, 4, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8],
[3, 4, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8],
[3, 5, 5, 6, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8],
[4, 4, 5, 6, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8],
[4, 5, 5, 5, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8],
[3, 5, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 8, 8],
[4, 4, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 8, 8],
[4, 5, 5, 6, 6, 7, 7, 7, 7, 7, 7, 7, 8, 8],
[5, 5, 5, 5, 6, 7, 7, 7, 7, 7, 7, 7, 8, 8],
[3, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 8, 8],
[4, 5, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 8, 8],
[5, 5, 5, 6, 6, 6, 7, 7, 7, 7, 7, 7, 8, 8],
[4, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 8, 8],
[5, 5, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 8, 8],
[5, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 8, 8],
[6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 8, 8],
[3, 4, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8],
[3, 5, 5, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8],
[4, 4, 5, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8],
[2, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8],
[3, 5, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8],
[4, 4, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8],
[4, 5, 5, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8],
[5, 5, 5, 5, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8],
[3, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 8],
[4, 5, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 8],
[5, 5, 5, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 8],
[4, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 8],
[5, 5, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 8],
[5, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 8],
[6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 8],
[2, 5, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7],
[3, 4, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7],
[2, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7],
[3, 5, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7],
[4, 4, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7],
[4, 5, 5, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7],
[3, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7],
[4, 5, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7],
[5, 5, 5, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7],
[4, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7],
[5, 5, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7],
[5, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7],
[6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7]]
# Trying to apply argument D with an 11-row in the 14/91 case yields
# four compatible column sequences, none of which work with a 12-row:
# [4, 4, 4, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 9]
# [4, 4, 4, 6, 7, 7, 7, 7, 7, 7, 7, 8, 8, 8]
# [3, 4, 5, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8]
# [4, 4, 4, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8]
assert_sols(14, 91, 0, [4] + [7]*7 + [-1]*6, 2, 2, suffix="_4_7x7")
# We thus first show that _any_ configuration using one of these four "nails"
# will only lead to UNSAT, which allows us to remove all 11+-row (3- pawns) sequences and more.
assert_sols(14, 91, 0, [4,4,7,7] + [-1]*10, 4, 4, suffix="_4477")
assert_sols(14, 91, 0, [4,5,5,6] + [-1]*10, 4, 4, suffix="_4556")
assert_sols(14, 91, 0, [4,6,6,6] + [-1]*10, 4, 4, suffix="_4666")
assert_sols(14, 91, 0, [5]*4 + [-1]*10, 4, 4, suffix="_5555")
assert_sols(14, 91, 0, [5,5,5,6] + [-1]*10, 5, 5, suffix="_5556")
assert_sols(14, 91, 0, [5,5,6,6,6] + [-1]*9, 5, 5, suffix="_55666")
assert_sols(14, 91, 0, [5] + [6]*5 + [-1]*8, 5, 5, suffix="_5_6x5")
assert_sols(14, 91, 0, [6]*10 + [-1]*4, 6, 6, [6]*7 + [-1]*7, suffix="_6x10")
assert_sols(14, 91, 0, [6]*9 + [7]*3 + [-1]*2, 6, 6, [6]*7 + [7]*3 + [-1]*4, suffix="_6x9")
assert_sols(14, 91, 0, [6]*8 + [7]*5 + [8], 6, 6, [6]*7 + [7]*5 + [-1]*2, suffix="_6x8")
assert_sols(14, 91, 1, [6]*7 + [7]*7, 6, 6, [6]*7 + [7]*7, suffix="_last")
for ds in sorted(pawnseqs2):
if all(not is_seq_excluded(ds, counts) for counts in [((4,1),(7,7)), ((2,1),), ((3,1),), ((4,2),(7,2)), ((4,1),(5,2),(6,1)), ((4,1),(6,3)), ((5,4),), ((5,3),(6,1)), ((5,2),(6,3)), ((5,1),(6,5)), ((6,10),), ((6,9),(7,3)), ((6,8),(7,5)), ((6,7),(7,7))]):
if sum(comb(c-1, 2) for c in [14-x for x in ds[::-1]][:11]) <= 2*comb(13,2):
print(ds) # nothing
print("->", ds)
Raw
zarankiewiczcases15.py
#!/usr/bin/env python3
from math import comb
from zarankiewicz import zaran_cnf
# https://drive.google.com/file/d/1kTiPW6--Rfc-Eal9EbxktB3AyIKJQ0ax/view?usp=sharing
def assert_sols(n, pawns, nsols, rcounts=None, rfloor=0, cfloor=0, ccounts=None, suffix="",
count_global=False, count_rem_row=True, count_rem_col=False):
body = f"{n}_{pawns}{suffix}"
cnf = zaran_cnf(n, 3, pawns)
if count_global:
cnf.set_global_count()
cnf.set_row_counts([-1] * n if rcounts == None else rcounts, rfloor, count_rem_row)
cnf.set_col_counts([-1] * n if ccounts == None else ccounts, cfloor, count_rem_col)
assert len(cnf.findallsols(f"{body}.cnf", nsols, proof=f"{body}.drat")) == nsols
# 15/104 pawns (15/121 edges) – 22 cases from argument A, 9 with 10+-rows (5- pawns) are immediately excluded by argument D
# forpart(v=121, if(sum(i=1, 15, binomial(v[i],3)) <= 2*binomial(15,3), print(vector(15, i, 15-v[16-i]),"," )), [0,15], 15)
pawnseqs = [[6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 10],
[6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 9, 9],
[6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 8, 8, 8, 9],
[5, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8, 9],
[6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 8, 8, 9],
[5, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 9],
[6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 9],
[5, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 9],
[6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 9],
[6, 6, 6, 6, 6, 6, 6, 7, 7, 8, 8, 8, 8, 8, 8],
[6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 8, 8, 8, 8, 8],
[5, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 8, 8, 8, 8],
[6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 8, 8, 8, 8],
[5, 5, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8, 8],
[5, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8, 8],
[6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8, 8],
[4, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8],
[5, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8],
[6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8],
[5, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8],
[6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8],
[6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7]]
assert_sols(15, 104, 0, [6]*3 + [7]*3 + [-1]*9, 6, 6, suffix="_6x3_7x3")
assert_sols(15, 104, 0, [6]*7 + [7]*2 + [8]*6, 6, 6, suffix="_6x7_7x2_8x6")
assert_sols(15, 104, 0, [6] + [7]*12 + [-1]*2, 6, 6, [6] + [7]*12 + [-1]*2, suffix="_6_7x12")
def is_seq_excluded(seq, counts):
return all(seq.count(c) >= m for (c, m) in counts)
for ds in sorted(pawnseqs):
if sum(comb(c-1, 2) for c in [15-x for x in ds[::-1]][:10]) <= 2*comb(14,2):
print(ds) # nothing
if all(not is_seq_excluded(ds, counts) for counts in [((4,1),), ((5,1),), ((6,3),(7,3)), ((6,7),(7,2),(8,6)), ((6,1),(7,12))]):
print("->", ds)
# 15/105 pawns (15/120 edges) – 80 cases from argument A, 11 with 11+-rows (4- pawns) are immediately excluded by argument D
pawnseqs2 = [[6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 8, 11],
[5, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 11],
[6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 11],
[6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 8, 9, 10],
[5, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 9, 10],
[6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 9, 10],
[6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 8, 8, 8, 8, 10],
[5, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 8, 8, 8, 10],
[6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 8, 8, 8, 10],
[5, 5, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8, 10],
[5, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8, 10],
[6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 8, 8, 10],
[4, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 10],
[5, 5, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 10],
[5, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 10],
[6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 10],
[4, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 10],
[5, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 10],
[6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 10],
[6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 8, 9, 9, 9],
[5, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 9, 9, 9],
[6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 9, 9, 9],
[6, 6, 6, 6, 6, 6, 6, 6, 7, 8, 8, 8, 8, 9, 9],
[5, 6, 6, 6, 6, 6, 7, 7, 7, 7, 8, 8, 8, 9, 9],
[6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 8, 8, 8, 9, 9],
[5, 5, 6, 6, 7, 7, 7, 7, 7, 7, 7, 8, 8, 9, 9],
[5, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 8, 8, 9, 9],
[6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 8, 8, 9, 9],
[5, 5, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 9, 9],
[5, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 8, 9, 9],
[6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 8, 9, 9],
[4, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 9, 9],
[5, 5, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 9, 9],
[5, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 9, 9],
[6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 9, 9],
[5, 6, 6, 6, 6, 6, 6, 7, 8, 8, 8, 8, 8, 8, 9],
[6, 6, 6, 6, 6, 6, 6, 6, 8, 8, 8, 8, 8, 8, 9],
[5, 6, 6, 6, 6, 6, 7, 7, 7, 8, 8, 8, 8, 8, 9],
[6, 6, 6, 6, 6, 6, 6, 7, 7, 8, 8, 8, 8, 8, 9],
[5, 5, 6, 6, 7, 7, 7, 7, 7, 7, 8, 8, 8, 8, 9],
[5, 6, 6, 6, 6, 7, 7, 7, 7, 7, 8, 8, 8, 8, 9],
[6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 8, 8, 8, 8, 9],
[4, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8, 8, 9],
[5, 5, 6, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8, 8, 9],
[5, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 8, 8, 8, 9],
[6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 8, 8, 8, 9],
[4, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8, 9],
[5, 5, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8, 9],
[5, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8, 9],
[6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8, 9],
[4, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 9],
[5, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 9],
[6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 9],
[5, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 9],
[6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 9],
[5, 6, 6, 6, 6, 6, 6, 8, 8, 8, 8, 8, 8, 8, 8],
[5, 5, 6, 6, 6, 7, 7, 7, 8, 8, 8, 8, 8, 8, 8],
[5, 6, 6, 6, 6, 6, 7, 7, 8, 8, 8, 8, 8, 8, 8],
[6, 6, 6, 6, 6, 6, 6, 7, 8, 8, 8, 8, 8, 8, 8],
[5, 5, 5, 7, 7, 7, 7, 7, 7, 8, 8, 8, 8, 8, 8],
[4, 6, 6, 6, 7, 7, 7, 7, 7, 8, 8, 8, 8, 8, 8],
[5, 5, 6, 6, 7, 7, 7, 7, 7, 8, 8, 8, 8, 8, 8],
[5, 6, 6, 6, 6, 7, 7, 7, 7, 8, 8, 8, 8, 8, 8],
[6, 6, 6, 6, 6, 6, 7, 7, 7, 8, 8, 8, 8, 8, 8],
[4, 5, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8, 8, 8, 8],
[4, 6, 6, 7, 7, 7, 7, 7, 7, 7, 8, 8, 8, 8, 8],
[5, 5, 6, 7, 7, 7, 7, 7, 7, 7, 8, 8, 8, 8, 8],
[5, 6, 6, 6, 7, 7, 7, 7, 7, 7, 8, 8, 8, 8, 8],
[6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 8, 8, 8, 8, 8],
[4, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8, 8, 8],
[5, 5, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8, 8, 8],
[5, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8, 8, 8],
[6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 8, 8, 8, 8],
[4, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8, 8],
[5, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8, 8],
[6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8, 8],
[5, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8],
[6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8],
[6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8],
[7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7]]
assert_sols(15, 105, 0, [5,5,6,7,7,7] + [-1]*9, 5, 5, suffix="_556777")
assert_sols(15, 105, 0, [5]*2 + [7]*6 + [-1]*7, 5, 5, suffix="_5x2_7x6")
assert_sols(15, 105, 0, [5,6,6,6,7,7] + [-1]*9, 5, 5, suffix="_566677")
assert_sols(15, 105, 0, [5] + [6]*6 + [8]*6 + [-1]*2, 5, 5, suffix="_5_6x6_8x6")
assert_sols(15, 105, 0, [5] + [7]*8 + [-1]*6, 5, 5, suffix="_5_7x8")
assert_sols(15, 105, 0, [6]*4 + [7]*3 + [-1]*8, 6, 6, suffix="_6x4_7x3")
assert_sols(15, 105, 0, [6]*3 + [7]*9 + [-1]*3, 7, 6, [7]*9 + [-1]*6, suffix="_6x3_7x9")
assert_sols(15, 105, 0, [6]*2 + [7]*11 + [-1]*2, 7, 6, [7]*11 + [-1]*4, suffix="_6x2_7x11")
assert_sols(15, 105, 0, [6] + [7]*13 + [8], 7, 6, [7]*13 + [-1]*2, suffix="_6_7x13")
assert_sols(15, 105, 1, [7]*15, 7, 7, [7]*15, suffix="_last")
for ds in sorted(pawnseqs2):
if sum(comb(c-1, 2) for c in [15-x for x in ds[::-1]][:11]) <= 2*comb(14,2):
print(ds) # nothing
if all(not is_seq_excluded(ds, counts) for counts in [((4,1),), ((5,2),(6,1),(7,3)), ((5,2),(7,6)), ((5,1),(6,3),(7,2)), ((5,1),(6,6),(8,6)), ((5,1),(7,8)), ((6,4),(7,3)), ((6,7),(8,4)), ((6,3),(7,9)), ((6,2),(7,11)), ((6,1),(7,13)), ((7,15),)]):
print("->", ds)
Raw
zarankiewiczpatterns
Optimal configurations for A350237. Those for n <= 15 have been proven to be all the
non-isomorphic (under row and column permutations and transpose) ones.
a(3) = 1
1..
...
...
a(4) = 3
1...
.1..
..1.
....
a(5) = 5
1....
.1...
..1..
...1.
....1
a(6) = 10
1.....
.11...
.1.1..
..1.1.
...11.
.....1
a(7) = 16
..11...
.1..1..
1....1.
1..11..
.1.1.1.
..1.11.
......1
a(8) = 22 (Fano plane + extra point)
..1.11..
...1.11.
1...1.1.
11...1..
.11...1.
1.11....
.1.11...
.......1
a(9) = 32
.......11
....111.1
..11..11.
..1111...
.1.1.1...
1..11...1
1.1..1.1.
1.1.1.1..
11....1..
.......11
....111..
..11..1..
.1.1.1..1
.11.1...1
1..11...1
1.1..1..1
1.1.1.11.
11....1..
.......11
....111.1
..11..11.
.1.1.1.1.
.11.1..1.
1..11....
1.1..1...
11....1..
1111....1
..11....1
.1.1...1.
1.1...1..
11...1...
.....1111
...1111..
..1.11.1.
.1..1.1.1
1...1..11
...1...11
..1...1.1
.1...11..
1.1.1....
...1111..
..1.11.1.
.1..1..11
1..1.1..1
11....11.
...1...11
..1...1.1
.1...1..1
1...1...1
...1111..
..1.11.1.
.1..1.11.
1....111.
1111.....
...1...11
..1...1.1
.1...1..1
1...1...1
....1111.
..1111...
.1.11.1..
1.1..1.1.
11....11.
a(10) = 40 (Petersen graph + diagonal)
11..11....
111...1...
.111...1..
..111...1.
1..11....1
1....1.11.
.1....1.11
..1..1.1.1
...1.11.1.
....1.11.1
a(11) = 52 (a(15) minus 4R4C)
..11....11.
.1....11.1.
1..1.1.1...
1.1.1.1....
...1.11.1.1
..1.1..11.1
.1.11.1...1
.11..1.1..1
1...11...11
11......111
....111111.
a(12) = 64 (a(15) minus 3R3C, or...)
1....11....1
...11.1..11.
...111.11...
.11...111...
.11..1...11.
1.1.1...1.1.
11.1...1.1..
..11..11..11
..11.1..11.1
.1..1.1.11.1
.1..11.1..11
1......11111
.1111...1...
1.11.1...1..
11.1..1...1.
111....1...1
1...11111...
.1..1111.1..
..1.1111..1.
...11111...1
1...1....111
.1...1..1.11
..1...1.11.1
...1...1111.
a(13) = 77 (a(15) minus 2R2C)
..1....1111..
..11111......
111........11
.1...11..11.1
.1..1.1.1.11.
.1.1.1.1.1.1.
.1.11..11...1
1....1111..1.
1...1.11.1..1
1..1.1..1.1.1
1..11....111.
..1.11.1..111
..11..1.11.11
a(14) = 91 (a(15) minus 1R1C)
....111....111
..11..1..11..1
.1.1.1..1.1.1.
.11.1...11.1..
1..11..1..11..
1.1..1.1.1..1.
11....111....1
....1111111...
..11..111..11.
.1.1.1.1.1.1.1
.11.1..1..1.11
1..11...11..11
1.1..1..1.11.1
11....1..1111.
a(15) = 105 (Kneser(6,2) or point adjacency matrix of GQ(2,2) + diagonal)
........1111111
....1111....111
..11..11..11..1
..1111..11....1
.1.1.1.1.1.1.1.
.1.11.1.1.1..1.
.11..11.1..11..
.11.1..1.11.1..
1..1.11..11.1..
1..11..11..11..
1.1..1.11.1..1.
1.1.1.1..1.1.1.
11....1111....1
11..11....11..1
1111........111
a(16) <= 128 (four Walsh matrices around a point):
11111111........
1.1.1.1.1.1.1.1.
11..11..11..11..
1..11..1.11..11.
1111....1111....
1.1..1.1.1.11.1.
11....11..1111..
1..1.11.1..1.11.
.11.1..1.11.1..1
..1111..11....11
.1.11.1.1.1..1.1
....1111....1111
.11..11.1..11..1
..11..11..11..11
.1.1.1.1.1.1.1.1
........11111111
x = 155, y = 96, rule = LifeHistory
47.3D.D.D.3D2.2D.3D4.D2.2D2.3D4.D2.D3.D5.3D.D.D.3D$48.D2.D.D.D3.D3.D
5.D.D.D.D.D5.D.D.D3.D6.D2.D.D.D$48.D2.3D.2D3.D2.2D4.3D.2D2.2D4.3D.D3.
D6.D2.3D.2D$48.D2.D.D.D5.D.D5.D.D.D.D.D5.D.D.D3.D6.D2.D.D.D$48.D2.D.D
.3D.2D2.3D3.D.D.D.D.3D3.D.D.3D.3D4.D2.D.D.3D2$32.D2.D2.D2.D2.D4.D2.2D
2.D2.D3.D2.D2.2D2.2D2.D.D.D2.2D4.2D2.D2.D3.D.D.3D.D2.D2.D2.D2.2D$32.
2D.D.D.D.2D.D4.D.D3.D.D.2D.2D.D.D.D.D.D.D.D.D.D.D5.D3.D.D.D3.D.D2.D2.
D.D.D.2D.D.D$32.D.2D.D.D.D.2D.2D.D2.D2.D.D.D.D.D.D.D.2D2.2D2.3D.D.D6.
D2.D.D.D3.D.D2.D2.D.D.D.D.2D2.D$32.D2.D.D.D.D2.D4.D3.D.D.D.D3.D.D.D.D
.D.D3.D.D.D.D7.D.D.D.D3.D.D2.D2.D.D.D.D2.D3.D$32.D2.D2.D2.D2.D4.D.2D
3.D2.D3.D2.D2.D.D.D3.D.D.D2.2D3.2D3.D2.3D2.2D2.D2.D2.D2.D2.D.2D3$77.D
$76.D.D$2.74D3.74D$.D151.D$D153.D2$D5.3D4.3D5.D.3D4.D.3D5.3D.3D4.3D.
3D5.D.D.3D6.3D.3D7.3D.D.D8.3D.3D9.3D.D12.D.3D.3D$D7.D4.D7.D.D.D4.D.D
9.D3.D6.D3.D5.D.D.D.D6.D5.D7.D3.D.D10.D3.D9.D.D.D12.D.D.D.D$D5.3D4.3D
5.D.D.D4.D.3D5.3D.3D4.3D.3D5.3D.D.D6.3D.3D7.3D.3D10.D3.D9.3D.D12.D.D.
D.3D$D7.D6.D5.D.D.D4.D.D.D5.D3.D8.D.D9.D.D.D8.D.D9.D.D3.D10.D3.D11.D.
D12.D.D.D3.D$D5.3D4.3D5.D.3D4.D.3D5.3D.3D4.3D.3D7.D.3D6.3D.3D7.3D3.D
10.D3.D9.3D.D12.D.3D.3D2$5D.6D.7D.8D.9D.10D.11D.12D.13D.14D.15D.16D.
17D$DA2.D.DA3.D.DA4.D.DA5.D.D2.2A3.D.D2.A.2A2.D.D7.2AD.D2A2.2A4.D.D2.
2A4.2A.D.DA4.2A4.AD.D2.A4.4A2.D.D4.3A4.3AD.D8.7AD$D3.D.D.A2.D.D.A3.D.
D.2A3.D.D.A2.A2.D.D3.A.2A.D.D4.3A.AD.D3A3.A3.D.D.A4.2A.A.D.D3.2A.A2.
2A.D.D2.5A6.D.D2.2A2.A2.2A2.AD.D4.4A4.3AD$D3.D.D2.A.D.D2.A2.D.D.A.A2.
D.DA4.A.D.DA3.A.A.D.D2.2A2.2A.D.D.3A3.A2.D.DA2.A.A.A3.D.D3.3A.2A3.D.D
3A8.2AD.D.A.A.A2.A.A.A.D.D2.2A2.2A2.2A2.AD$5D.D4.D.D3.A.D.D2.A.A.D.DA
2.2A2.D.D2A3.A2.D.D2.4A3.D.D2.3A3.A.D.DA.A.A.A4.D.D.2A3.3A3.D.D.A3.2A
2.2A.AD.D.2A.A3.2A.A2.D.D2.4A2.2A4.AD$6.6D.D4.AD.D3.2A.D.D.A.A.A.D.D.
2A3.A.D.D.A.A.A3.D.DA2.2A4.AD.D3.A.2A.A.AD.D.2A2.A3.2A.D.D.A2.A.A.A.
2A.D.DA2.2A2.A2.2A2.D.D.A.A.A.A.A.A.A.D$13.7D.D5.AD.D2.A.2A.D.DA.2A4.
D.DA2.2A3.AD.DA4.A.2A.D.D2.A.A2.2A.AD.DA.A.A3.A.A.D.D.A.A.A.A.A.A.D.D
A.A2.A.A.A2.A.D.D.A.2A.A.A.A2.A.D$21.8D.D6.AD.D.A.2A3.D.DA.A2.A.A.D.D
.A4.A.2AD.D.A.2A.A3.AD.D2A.A3.A.A2.D.D.A.2A2.2A3.AD.D2A4.3A4.AD.D.2A
2.2A.A2.2A2.D$30.9D.D7.AD.DA.A.A.A2.D.D2.A2.A.A.AD.D.2A2.A.A2.AD.D2.
2A2.2A2.2AD.DA4.4A2.A.D.D4.7A3.D.D.2A.A2.A.2A.A2.D$40.10D.D2A4.A2.D.D
3.A.2A.A.D.DA3.2A3.2AD.D2.2A.A2.2A.AD.DA3.A.2A.A2.AD.D2.2A2.3A2.2A.D.
DA2.A.2A2.2A.A2.D$51.11D.D4.A.2A.AD.D2A6.3AD.D.A2.A.A.2A.AD.DA2.A.A2.
A.A.AD.D.A.A.A.A.A.A.AD.DA2.2A2.2A2.2A2.D$51.D7.2AD.12D.D4.6A.D.D.A2.
2A.A2.2AD.DA2.2A4.3A.D.D.2A.A2.A2.A.2AD.DA.A2.A.2A.A2.A.D$51.D4.3A2.D
14.13D.DA6.5AD.D2.A.2A.A2.3AD.DA2.2A3.2A2.2AD.DA.A.A.A2.A.A.A.D$51.D
2.2A2.A2.D28.14D.D2.2A2.A.2A.2AD.DA.A2.A2.A.2A.AD.D2A4.4A4.AD$51.D.A.
A.A2.AD28.D.4A3.A3.D.15D.D2A4.A2.4A.D.D2A2.2A4.2A2.AD$51.D.2A.A3.AD
28.DA.2A.A3.A2.D17.16D.D4A8.3AD$51.DA2.2A3.AD28.D2A.A2.A3.A.D34.17D$
51.DA.A2.A2.AD28.D3A4.A3.AD$51.DA.A.A.2A.D28.DA3.5A3.D$51.D2A4.A2.D
28.D.A2.4A.A2.D$51.11D28.D2.A.4A2.A.D$51.D7.2AD28.D3.5A3.AD$51.D4.3A.
AD28.DA3.A4.3AD$51.D2.2A2.2A.D28.D.A3.A2.A.2AD$51.D.A.A.A.A.D28.D2.A
3.A.2A.AD$51.D.2A.A2.A.D28.D3.A3.4A.D$51.DA2.2A4.D28.14D$51.DA.A2.A3.
D$51.D2A4.A2.D$51.D4A4.AD$51.11D$51.D2.2A4.AD$51.D.A.A3.A.D$51.DA.A3.
A2.D$51.D2A3.A3.D$51.D5.4AD$51.D3.4A2.D$51.D2.A.2A.A.D$51.D.A2.A.A.AD
$51.DA3.A2.2AD$51.11D$51.D3.A3.2AD$51.D2.A3.A.AD$51.D.A3.2A2.D$51.DA.
A.A4.D$51.D3.4A2.D$51.D2.A.2A.A.D$51.D.A2.A2.2AD$51.DA2.A.A2.AD$51.D
2A4.2A.D$51.11D$51.D3.A3.2AD$51.D2.A3.A.AD$51.D.A3.A2.AD$51.DA3.A3.AD
$51.D3.4A2.D$51.D2.A.2A.A.D$51.D.A2.A.2A.D$51.DA4.3A.D$51.D4A5.D$51.
11D$51.D3.A3.2AD$51.D2.A3.A.AD$51.D.A3.A2.AD$51.DA3.A3.AD$51.D4.4A.D$
51.D2.4A3.D$51.D.A.2A.A2.D$51.DA.A2.A.A.D$51.D2A4.2A.D$51.11D!
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment