1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
|
import pycosat
N = 8
def v(i, j):
return N * i + j + 1
def to_cnf(vs, eq=False):
if eq:
yield vs
for v1 in vs:
for v2 in vs:
if v1 < v2:
yield [-v1, -v2]
def queens_clauses():
# rows and columns
for i in range(N):
for clause in to_cnf([v(i, j) for j in range(N)], True):
yield clause
for clause in to_cnf([v(j, i) for j in range(N)], True):
yield clause
# diagonal
for i in range(N - 1):
for clause in to_cnf([v(j, i + j) for j in range(N - i)]):
yield clause
for i in range(1, N - 1):
for clause in to_cnf([v(j + i, j) for j in range(N - i)]):
yield clause
for i in range(N - 1):
for clause in to_cnf([v(j, N - 1 - (i + j)) for j in range(N - i)]):
yield clause
for i in range(1, N - 1):
for clause in to_cnf([v(j + i, N - 1 - j) for j in range(N - i)]):
yield clause
def solve():
clauses = queens_clauses()
# solve the SAT problem
for sol in pycosat.itersolve(clauses):
sol = set(sol)
for i in range(N):
print(''.join('Q' if v(i, j) in sol else '.' for j in range(N)))
print('')
if __name__ == '__main__':
solve()
|
