1# -*- mode: python; coding: utf-8 -*- 2# Copyright (C) 2010, 2011, 2012, 2014, 2019 Laboratoire de Recherche et 3# Développement de l'EPITA. 4# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 5# (LIP6), département Systèmes Répartis Coopératifs (SRC), Université 6# Pierre et Marie Curie. 7# 8# This file is part of Spot, a model checking library. 9# 10# Spot is free software; you can redistribute it and/or modify it 11# under the terms of the GNU General Public License as published by 12# the Free Software Foundation; either version 3 of the License, or 13# (at your option) any later version. 14# 15# Spot is distributed in the hope that it will be useful, but WITHOUT 16# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY 17# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public 18# License for more details. 19# 20# You should have received a copy of the GNU General Public License 21# along with this program. If not, see <http://www.gnu.org/licenses/>. 22 23# Python translation of the C++ example from the BuDDy distribution. 24# (compare with buddy/examples/queen/queen.cxx) 25 26import sys 27from buddy import * 28 29 30def build(i, j): 31 """ 32 Build the requirements for all other fields than (i,j) assuming 33 that (i,j) has a queen. 34 """ 35 a = b = c = d = bddtrue 36 37 # No one in the same column. 38 for l in side: 39 if l != j: 40 a &= X[i][j] >> -X[i][l] 41 42 # No one in the same row. 43 for k in side: 44 if k != i: 45 b &= X[i][j] >> -X[k][j] 46 47 # No one in the same up-right diagonal. 48 for k in side: 49 ll = k - i + j 50 if ll >= 0 and ll < N: 51 if k != i: 52 c &= X[i][j] >> -X[k][ll] 53 54 # No one in the same down-right diagonal. 55 for k in side: 56 ll = i + j - k 57 if ll >= 0 and ll < N: 58 if k != i: 59 c &= X[i][j] >> -X[k][ll] 60 61 global queen 62 queen &= a & b & c & d 63 64 65# Get the number of queens from the command-line, or default to 8. 66if len(sys.argv) > 1: 67 N = int(argv[1]) 68else: 69 N = 8 70 71side = range(N) 72 73# Initialize with 100000 nodes, 10000 cache entries and NxN variables. 74bdd_init(N * N * 256, 10000) 75bdd_setvarnum(N * N) 76 77queen = bddtrue 78 79# Build variable array. 80X = [[bdd_ithvar(i*N+j) for j in side] for i in side] 81 82# Place a queen in each row. 83for i in side: 84 e = bddfalse 85 for j in side: 86 e |= X[i][j] 87 queen &= e 88 89# Build requirements for each variable(field). 90for i in side: 91 for j in side: 92 sys.stdout.write("Adding position %d, %d\n" % (i, j)) 93 build(i, j) 94 95# Print the results. 96sys.stdout.write("There are %d solutions, one is:\n" % 97 bdd_satcount(queen)) 98solution = bdd_satone(queen) 99bdd_printset(solution) 100 101from spot import nl_cout 102nl_cout() 103 104# Cleanup all BDD variables before calling bdd_done(), otherwise 105# bdd_delref will be called after bdd_done() and this is unsafe in 106# optimized builds. 107X = e = queen = solution = 0 108bdd_done() 109