Lesson 7

This module allows you to write more compact code because some standard things are already implemented there. For example, it has a class \(\texttt{IDPool}\) that is responsible for storing unique numbers for variables (this is easy to do with a hash table), so you don't have to write methods like \(\texttt{varnum}\) yourself, as in our code above. There are also built-in methods that allow you to write linear constraints of the form “sum of given literals greater/less/equal to \(k\)” in one line (these are called cardinality constraints). These methods need to be passed the instance of the \(\texttt{IDPool}\) class being used, because to write these constraints compactly they may introduce auxiliary variables.

from itertools import product
from pysat.solvers import Solver
from pysat.card import *
from pysat.formula import IDPool, CNF

n = 30
pool, clauses = IDPool(), CNF()

for row in range(n):
    clauses.extend(CardEnc.equals(
        lits=[pool.id((row, column)) for column in range(n)],
        bound=1, vpool=pool
    ))

for column in range(n):
    clauses.extend(CardEnc.equals(
        lits=[pool.id((row, column)) for row in range(n)],
        bound=1, vpool=pool
    ))

for row, column in product(range(n), repeat=2):
    clauses.extend(CardEnc.atmost(
        lits=[pool.id((r, c)) for r, c in product(range(n), repeat=2) if r - c == row - column],
        bound=1, vpool=pool
    ))
    clauses.extend(CardEnc.atmost(
        lits=[pool.id((r, c)) for r, c in product(range(n), repeat=2) if r + c == row + column],
        bound=1, vpool=pool
    ))

solver = Solver(bootstrap_with=clauses)
solver.solve()
model = solver.get_model()

for row in range(n):
    for column in range(n):
        print('X' if pool.id((row, column)) in model else '*', end='')
    print()

*************************X****
****************X*************
********************X*********
**********X*******************
**************X***************
***********X******************
******************X***********
**************************X***
X*****************************
**X***************************
*********X********************
************X*****************
********X*********************
************************X*****
****************************X*
***********************X******
*************X****************
**********************X*******
***X**************************
*********************X********
***************X**************
*******X**********************
*****X************************
***************************X**
******X***********************
*X****************************
*****************************X
****X*************************
*******************X**********
*****************X************