Uniquising a Disconnect Four puzzle (PSE #111929)

analyse.py

#!/usr/bin/env python3

with open("sols", 'r') as f:
    sols = [s.strip() for s in f.readlines()]

def checksols(remsols, start, remlevels):
    if len(remsols) == 1:
        raise ValueError(remsols[0])
    if remlevels == 0:
        return
    for i in range(start, 61):
        if remlevels > 1:
            print('*' * remlevels, i)
        remsols_p = list(filter(lambda sol: sol[i] == '+', sols))
        remsols_m = list(filter(lambda sol: sol[i] == '-', sols))
        if not remsols_p or not remsols_m:
            continue # this variable is useless at the current level
        checksols(remsols_p, i+1, remlevels-1)
        checksols(remsols_m, i+1, remlevels-1)
checksols(sols, 0, 3)

usolsets = set()
for i in range(61):
    for s in "+-":
        remsols = list(filter(lambda sol: sol[i] == s, sols))
        if len(remsols) == len(sols):
            print(f"{i+1}{s} forced")
        if len(remsols) == 8:
            usolsets.add(frozenset(remsols))
            diffis = []
            for cand in range(61):
                for j in range(8):
                    if remsols[j-1][cand] != remsols[j][cand]:
                        diffis.append(cand+1)
                        break
            print(f"{i+1}{s}", diffis)
print(usolsets)
print(len(usolsets))

findsols.py

#!/usr/bin/env python3
import re
from subprocess import run
import numpy as np
lit_re = re.compile(r"-?\d+")
cnfn = "dc4.cnf"

# Run `./make-sat-problem.py | tee sols` to see progress and get an output file at the same time

xs = (11, 21, 26, 27, 35, 45, 49, 51, 57, 62, 69, 70, 71, 74, 75, 78, 89, 92, 93)
os = (3, 4, 7, 8, 12, 20, 33, 34, 37, 43, 46, 68, 72, 80, 82, 83, 90, 95, 97, 99)
n_unknown = 0
n_x = 0
n_o = 0
L = []
for v in range(1, 101):
    if v in xs:
        n_x += 1
        L.append(61+n_x)
    elif v in os:
        n_o += 1
        L.append(80+n_o)
    else:
        n_unknown += 1
        L.append(n_unknown)

bvars = np.array(L).reshape(10, 10)
# print(bvars); 0 / 0
clauses = []
for i in range(10):
    for j in range(7):
        row = bvars[i,j:j+4]
        clauses.append(list(row))
        clauses.append(list(-row))
        col = bvars[j:j+4,i]
        clauses.append(list(col))
        clauses.append(list(-col))
for i in range(7):
    for j in range(7):
        M = bvars[i:i+4,j:j+4]
        fd = np.diag(M)
        clauses.append(list(fd))
        clauses.append(list(-fd))
        bd = np.diag(np.fliplr(M))
        clauses.append(list(bd))
        clauses.append(list(-bd))
# Manually eliminate unit clauses
for cl in clauses:
    for v in range(62, 81): # x, 1
        if v in cl:
            cl.clear()
            break
        elif -v in cl:
            cl.remove(-v)
    for v in range(81, 101): # o, 0
        if -v in cl:
            cl.clear()
            break
        elif v in cl:
            cl.remove(v)
clauses = list(map(list, {tuple(cl): 0 for cl in filter(bool, clauses)}.keys()))
nvars = max({abs(l) for cl in clauses for l in cl})
nclauses = len(clauses)
with open(cnfn, 'w') as f:
    print(f"p cnf {nvars} {nclauses}", file=f)
    for clause in clauses:
        print(" ".join(map(str, clause + [0])), file=f)

nsols = 0
while True:
    proc = run(["./cadical", "-q", cnfn], capture_output=True, encoding="utf-8")
    if proc.returncode != 10:
        break
    nsols += 1
    sol = list(map(int, lit_re.findall(proc.stdout)[:-1]))
    print("".join('+' if l > 0 else '-' for l in sol))
    with open(cnfn, 'r') as f:
        contents = f.read().partition("\n")[2]
    with open(cnfn, 'w') as f:
        print(f"p cnf {nvars} {nclauses+nsols}", file=f)
        f.write(contents)
        print(" ".join(str(-x) for x in sol), "0", file=f)