bddnqueen.py 2.94 KB
Newer Older
1
# -*- mode: python; coding: utf-8 -*-
2 3
# Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et
# Développement de l'EPITA.
4 5 6
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6
# (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
# Pierre et Marie Curie.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
#
# This file is part of Spot, a model checking library.
#
# Spot is free software; you can redistribute it and/or modify it
# under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 2 of the License, or
# (at your option) any later version.
#
# Spot is distributed in the hope that it will be useful, but WITHOUT
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
# License for more details.
#
# You should have received a copy of the GNU General Public License
# along with Spot; see the file COPYING.  If not, write to the Free
# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
# 02111-1307, USA.

25 26 27 28 29
# Python translation of the C++ example from the BuDDy distribution.
# (compare with buddy/examples/queen/queen.cxx)

import sys
from buddy import *
30
from spot import nl_cout
31 32 33 34 35

# Build the requirements for all other fields than (i,j) assuming
# that (i,j) has a queen.
def build(i, j):
    a = b = c = d = bddtrue
36

37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92
    # No one in the same column.
    for l in side:
        if l != j:
            a &= X[i][j] >> -X[i][l]

    # No one in the same row.
    for k in side:
        if k != i:
            b &= X[i][j] >> -X[k][j]

    # No one in the same up-right diagonal.
    for k in side:
        ll = k - i + j
        if ll >= 0 and ll < N:
            if k != i:
                c &= X[i][j] >> -X[k][ll]

    # No one in the same down-right diagonal.
    for k in side:
        ll = i + j - k
        if ll >= 0 and ll < N:
            if k != i:
                c &= X[i][j] >> -X[k][ll]

    global queen
    queen &= a & b & c & d



# Get the number of queens from the command-line, or default to 8.
if len(sys.argv) > 1:
    N = int(argv[1])
else:
    N = 8

side = range(N)

# Initialize with 100000 nodes, 10000 cache entries and NxN variables.
bdd_init(N * N * 256, 10000)
bdd_setvarnum(N * N)

queen = bddtrue

# Build variable array.
X = [[bdd_ithvar(i*N+j) for j in side] for i in side]

# Place a queen in each row.
for i in side:
    e = bddfalse
    for j in side:
        e |= X[i][j]
    queen &= e

# Build requirements for each variable(field).
for i in side:
    for j in side:
93
        sys.stdout.write("Adding position %d, %d\n" % (i, j))
94 95 96
        build(i, j)

# Print the results.
97 98
sys.stdout.write("There are %d solutions, one is:\n" %
                 bdd_satcount(queen))
99 100
solution = bdd_satone(queen)
bdd_printset(solution)
101
nl_cout()
102

103 104 105 106
# Cleanup all BDD variables before calling bdd_done(), otherwise
# bdd_delref will be called after bdd_done() and this is unsafe in
# optimized builds.
X = e = queen = solution = 0
107
bdd_done()