CNF.py

class CNF:
    def __init__(self, filename):
        self.file = open(filename, "w")
        self.clauses = []
        self.variables = 0

    def add(self, clause):
        # takes a list of variables, adds it as a clause to our output
        #print("Adding clause", clause)
        self.clauses.append(" ".join([str(x) for x in clause])+" 0\n")

    def write(self):
        # writes to file
        self.file.write("p cnf "+str(self.variables)+" "+str(len(self.clauses))+"\n")
        self.file.writelines(self.clauses)

    def close(self):
        # closes file
        self.file.close()

n-queens.py

#!/usr/bin/env python3
from cnf import CNF

SIZE = int(input("Enter number: "))

outp = CNF(str(SIZE)+"-queens.cnf")
outp.variables = SIZE*SIZE;

def pair2int(n,p):
    return SIZE*(n-1)+p

def get_clauses(x, y):
    outp = []
    own_num = pair2int(y,x)
    for i in range(x+1, SIZE+1): # go through row
        num = pair2int(y,i)
        outp.append([-own_num, -num])
    for i in range(y+1, SIZE+1): # go through column
        num = pair2int(i,x)
        outp.append([-own_num, -num])
    for i in range(1, min(SIZE - x + 1, SIZE - y + 1)): # go through diagonal down
        num = pair2int(y+i, x+i)
        outp.append([-own_num, -num])
    for i in range(1, min(SIZE - x + 1, y)): # go through diagonal up
        num = pair2int(y-i, x+i)
        outp.append([-own_num, -num])
    return outp

# generate all the excluding clauses (cannot be multiple per row)
for x in range(1, SIZE+1):
    for y in range(1, SIZE+1):
        for clause in get_clauses(x, y):
            outp.add(clause)

# generate all the including clauses (must be 1 per row)
for y in range(1, SIZE+1):
    clause = []
    for x in range(1, SIZE+1):
        clause.append(pair2int(y, x))
    outp.add(clause)

outp.write()

n-towers.py

#!/usr/bin/env python3
from cnf import CNF

SIZE = int(input("Enter number: "))

outp = CNF(str(SIZE)+"-towers.cnf")
outp.variables = SIZE*SIZE;

def pair2int(n,p):
    return SIZE*(n-1)+p

def get_clauses(x, y):
    outp = []
    own_num = pair2int(y,x)
    for i in range(x+1, SIZE+1): # go through row
        num = pair2int(y,i)
        outp.append([-own_num, -num])
    for i in range(y+1, SIZE+1): # go through column
        num = pair2int(i,x)
        outp.append([-own_num, -num])
    return outp

# generate all the excluding clauses (cannot be multiple per row)
for x in range(1, SIZE):
    for y in range(1, SIZE):
        for clause in get_clauses(x,y):
            outp.add(clause)

# generate all the including clauses (must be 1 per row)
for y in range(1, SIZE+1):
    clause = []
    for x in range(1, SIZE+1):
        clause.append(pair2int(y, x))
    outp.add(clause)

outp.write()