A very bad n-queens solver using miniSAT

n-queens.py

# write DIMACS file for getting n-queens soln using miniSAT

import sys
import subprocess
from itertools import combinations

n = int(sys.argv[1])

total_vars = n ** 2

prim_clauses = []

# Row exclusivity clause:
for row in range(n):
    for i in range(n):
        for j in range(i + 1, n):
            prim_clauses.append(f"-{row * n + i + 1} -{row * n + j + 1} 0")

# Column exclusivity clause:
for col in range(n):
    for i in range(n):
        for j in range(i + 1, n):
            prim_clauses.append(f"-{i * n + col + 1} -{j * n + col + 1} 0")

# Forward diagonal exclusivity clause:
for i in range(1, total_vars + 1):
    if i % n == 0:
        continue
    d = n + 1
    while i + d <= total_vars and (i + d - 1) % n > (i - 1) % n:
        prim_clauses.append(f"-{i} -{i + d} 0")
        d += n + 1

# Backward diagonal exclusivity clause:
for i in range(1, total_vars + 1):
    if i % n == 1:
        continue
    d = n - 1
    while i + d <= total_vars and (i + d - 1) % n < (i - 1) % n:
        prim_clauses.append(f"-{i} -{i + d} 0")
        d += n - 1

# Start with 2 queens and continue till we find no solutions
for num_queens in range(2, n + 1):
    clauses = prim_clauses.copy()
    for valid in combinations(range(1, total_vars + 1), total_vars - num_queens + 1):
        clauses.append(" ".join(map(str, valid)) + " 0")
    with open(f"{num_queens}-queens.cnf", "w") as f:
        f.write(f"p cnf {total_vars} {len(clauses)}\n")
        f.write("\n".join(clauses))
    print("=" * 8, f"Running miniSAT for {num_queens} queens", "=" * 8)
    result = subprocess.run(["./bin/minisat", f"{num_queens}-queens.cnf", f"{num_queens}-queens-out.cnf"], capture_output=True, text=True)
    if "UNSAT" in result.stdout:
        print("UNSAT")
        break
    # If SAT, find all solutions
    sol = 0
    while "SAT" in result.stdout:
        with open(f"{num_queens}-queens-out.cnf", "r") as f:
            lines = f.readlines()
            if len(lines) < 2:
                break
            new_clause = [x for x in map(int, lines[1].strip().split()) if x > 0]
        print(f"Found solution: {new_clause}")
        sol += 1
        new_clause = [-x for x in new_clause]
        clauses.append(" ".join(map(str, new_clause)) + " 0")
        with open(f"{num_queens}-queens.cnf", "w") as f:
            f.write(f"p cnf {total_vars} {len(clauses)}\n")
            f.write("\n".join(clauses))
        result = subprocess.run(["./bin/minisat", f"{num_queens}-queens.cnf", f"{num_queens}-queens-out.cnf"], capture_output=True, text=True)
    print(f"Total solutions for {num_queens} queens: {sol}")