sat-nqueens

nqueens.py

n = int(input('enter N: '))

clauses = []
clauses_count = 0

i = 0
while i < n * n:
    row = []
    current_clauses = []
    for k in range(i, i + n):
        row.append(k + 1)
    row.append(0)
    clauses_count += 1
    for idx, j in enumerate(row):
        for k in row[idx:]:
            if j == k or k == 0: continue
            current_clauses.append(' '.join([str(-j), str(-k), '0']))
            clauses_count += 1
    clauses.append(' '.join([str(x) for x in row]))
    clauses.append('\n'.join(current_clauses))

    i += n

i = 1
while i <= n:
    row = []
    current_clauses = []
    for k in range(n):
        row.append(i + k * n)
    row.append(0)
    clauses_count += 1
    for idx, j in enumerate(row):
        for k in row[idx:]:
            if j == k or k == 0: continue
            current_clauses.append(' '.join([str(-j), str(-k), '0']))
            clauses_count += 1
    clauses.append(' '.join([str(x) for x in row]))
    clauses.append('\n'.join(current_clauses))

    i += 1



print(f'p cnf {n * n} {clauses_count}')
print('\n'.join(clauses))