勇闖新世界︰ 《 pyDatalog 》【小品】之八皇后問題

什麼是『知識』?長久以來,西方的主流思潮中有一個稱之為『JTB』 justified true belief  的『經確證的真信念』之理論,它是這麼定義『知識』與『知道』的︰

The JTB account of knowledge is the claim that knowledge can be conceptually analyzed as justified true belief — which is to say that the meaning of sentences such as “Smith knows that it rained today” can be given with the following set of necessary and sufficient conditions:

A subject S knows that a proposition P is true if and only if:

P is true, and
S believes that P is true, and
S is justified in believing that P is true

JTB 理論對於知識的解釋是︰宣稱知識可以概念解析為經確證的真信念 ── 這就是說『史密斯知道今天下雨』一句話的意義,可以用如下之充份與必要的條件來給定︰

 

 

一位主體 S 知道一個命題 P 是真的,若且唯若︰

一、 P 是真的,且
二、S 相信 P 是真的,而且
三、S 有經確證的真信念相信P 是真的

在 這個定義下『知道□』意味著有『□的知識』,因為『知識』是由『真的命題』構成,所以必須有第一條件;如果某甲 『聽說』過 □ ,但是不相信,或者以為它是『假的』,當然不能說他知道□;再者雖說某甲相信□,卻出於無『理據』,比方說從『不知哪裡』得來的,一但『爭論』將無法『辯 護其說』,所以也不能講他真知道□。如此說來,這個定義該是很完善的了,但是卻受到美國哲學家 Edmund Gettier 的反駁,他說即使上述的三條要件都得到了滿足,有些情況下我們仍然不能聲稱『某甲知道□』── 這就是知名的『葛梯爾問題』 ──。如今葛梯爾問題之多都成『問題集』了,於此就說一個經典的『空地上的奶牛』 The Cow in the field 問題︰

一 位農民正擔心自己獲獎的奶牛走失了;這時送奶工到了農場,告訴他說︰不必擔心,他看到那頭奶牛在附近的一塊空地上。雖然農民很相信送奶工,但是他還是親自 的望了望,見著了熟悉的黑白相間之物,感覺滿意的放下心來。隔了一會兒,送奶工走過那塊空地想再次確認,他發現那頭奶牛確實是在那裡,不過現在它躲進樹林 裡了,並且空地上還有著一大張黑白相間的紙纏在樹上。顯然是,農民把這張紙錯認成那頭奶牛的了;於是問題就來了,雖然奶牛一直都在空地上,假使農民說自己 知道奶牛在空地上時,此時這句話是正確的嗎?……

─── 摘自《基因改寫 ── Thue 改寫系統之補充《二》

 

若說『相信』產生『信念』,『信念』的強度,將『可信』之『反例』給『排除』後得到加強。『懷疑』卻因『不可信』之『反例 』『排除』不了而引發。如是看來,處於『真』和『假』兩極之間的『信念』與『懷疑』往往在一者過強之時,向另一者方向變化 ,恐由於『事例眾』,『反例』就『多』之故。科學探究大自然的『知識』,也可以說是『真』和『假』的『過濾器』,『排除』假的,保留『真』的,那麼在『科學』發達的今日,是否也意味著『懷疑』之心也加強了呢?人類想知道『宇宙有沒有』其它像人類一樣高等生命之情又來自哪裡??現今能用的辦法,究其實果真可『確定』的講︰我們知道我們並不孤單,還有生命在時空的涯角呢 !!

就讓我們借著一八四八年,馬克斯‧貝瑟爾 Max Bezzel ,一位國際西洋棋棋手,提出的『八皇后問題

八皇后問題是一個以西洋棋為背景的問題:如何能夠在 8×8 的西洋棋棋盤上放置八個皇后,使得任何一個皇后都無法直接吃掉其他的皇后?為了達到此目的,任兩個皇后都不能處於同一條橫行、縱行或斜線上。

追朔了解一下 pyDatalog 範例中所用的方法,查核一下我們能否講︰我們知道 pyDatalog 這個語言的用法。

關於八皇后問題的解法,維基百科已作了很好的總結︰

Eight queens puzzle

Finding all solutions to the eight queens puzzle is a good example of a simple but nontrivial problem. For this reason, it is often used as an example problem for various programming techniques, including nontraditional approaches such as constraint programming, logic programming or genetic algorithms. Most often, it is used as an example of a problem that can be solved with a recursive algorithm, by phrasing the n queens problem inductively in terms of adding a single queen to any solution to the problem of placing n−1 queens on an n-by-n chessboard. The induction bottoms out with the solution to the ‘problem’ of placing 0 queens on the chessboard, which is the empty chessboard.

This technique is much more efficient than the naïve brute-force search algorithm, which considers all 648 = 248 = 281,474,976,710,656 possible blind placements of eight queens, and then filters these to remove all placements that place two queens either on the same square (leaving only 64!/56! = 178,462,987,637,760 possible placements) or in mutually attacking positions. This very poor algorithm will, among other things, produce the same results over and over again in all the different permutations of the assignments of the eight queens, as well as repeating the same computations over and over again for the different sub-sets of each solution. A better brute-force algorithm places a single queen on each row, leading to only 88 = 224 = 16,777,216 blind placements.

It is possible to do much better than this. One algorithm solves the eight rooks puzzle by generating the permutations of the numbers 1 through 8 (of which there are 8! = 40,320), and uses the elements of each permutation as indices to place a queen on each row. Then it rejects those boards with diagonal attacking positions. The backtracking depth-first search program, a slight improvement on the permutation method, constructs the search tree by considering one row of the board at a time, eliminating most nonsolution board positions at a very early stage in their construction. Because it rejects rook and diagonal attacks even on incomplete boards, it examines only 15,720 possible queen placements. A further improvement, which examines only 5,508 possible queen placements, is to combine the permutation based method with the early pruning method: the permutations are generated depth-first, and the search space is pruned if the partial permutation produces a diagonal attack. Constraint programming can also be very effective on this problem.

An alternative to exhaustive search is an ‘iterative repair’ algorithm, which typically starts with all queens on the board, for example with one queen per column.[8] It then counts the number of conflicts (attacks), and uses a heuristic to determine how to improve the placement of the queens. The ‘minimum-conflicts’ heuristic — moving the piece with the largest number of conflicts to the square in the same column where the number of conflicts is smallest — is particularly effective: it finds a solution to the 1,000,000 queen problem in less than 50 steps on average. This assumes that the initial configuration is ‘reasonably good’ — if a million queens all start in the same row, it will obviously take at least 999,999 steps to fix it. A ‘reasonably good’ starting point can for instance be found by putting each queen in its own row and column so that it conflicts with the smallest number of queens already on the board.

Note that ‘iterative repair’, unlike the ‘backtracking’ search outlined above, does not guarantee a solution: like all hillclimbing (i.e., greedy) procedures, it may get stuck on a local optimum (in which case the algorithm may be restarted with a different initial configuration). On the other hand, it can solve problem sizes that are several orders of magnitude beyond the scope of a depth-first search.

Eight-queens-animation.gif

This animation illustrates backtracking to solve the problem. A queen is placed in a column that is known not to cause conflict. If a column is not found the program returns to the last good state and then tries a different column.

 

有興趣 N 皇后問題的多種 Python 程式解法者,可以參考

http://rosettacode.org/wiki/N-Queens#Python 》這個網頁。

 

此處特舉 Raymond Hettinger 先生於二零零九年二月十號所發表的

Eight queens. Six lines. (Python recipe)》處方︰

What six lines of Python can do

from itertools import permutations

n = 8
cols = range(n)
for vec in permutations(cols):
    if (n == len(set(vec[i]+i for i in cols))
          == len(set(vec[i]-i for i in cols))):
        print vec

 

Solver for the eight queens puzzle:
http://en.wikipedia.org/wiki/Eight_queens_puzzle

Computes all 92 solutions for eight queens. By setting n to different values, other sized puzzles can be solved.

The output is presented in vector form (each number represents the column position of a queen on consecutive rows). The vector can be pretty printed with this function:

def board(vec):
    '''Translate column positions to an equivalent chess board.

    >>> board([0, 4, 7, 5, 2, 6, 1, 3])
    Q-------
    ----Q---
    -------Q
    -----Q--
    --Q-----
    ------Q-
    -Q------
    ---Q----

    '''

    for col in vec:
        s = ['-'] * len(vec)
        s[col] = 'Q'
        print ''.join(s)
    print

 

With the solution represented as a vector with one queen in each row, we don’t have to check to see if two queens are on the same row. By using a permutation generator, we know that no value in the vector is repeated, so we don’t have to check to see if two queens are on the same column. Since rook moves don’t need to be checked, we only need to check bishop moves.

The technique for checking the diagonals is to add or subtract the column number from each entry, so any two entries on the same diagonal will have the same value (in other words, the sum or difference is unique for each diagnonal). Now all we have to do is make sure that the diagonals for each of the eight queens are distinct. So, we put them in a set (which eliminates duplicates) and check that the set length is eight (no duplicates were removed).

Any permutation with non-overlapping diagonals is a solution. So, we print it and continue checking other permutations.

 

這六行『派生』 Python 程式果然不同凡響,構造精妙且論理清楚。這就是 pyDatalog 解決八皇后問題的邏輯基礎。為了明白 pyDatalog 的程式,還得知道那個語言的幾件事︰

‧ 有不同『參數個數』之『同名』述詞為『不同述詞』。

‧ 『同名』述詞的多個定義是『邏輯 or 』。

‧ 『變元』是『子句參數』,其值不能自跨『子句』。

‧ 『變元值』的『引用』以『變元名』為之。

# give me all the X and Y so that X is 2 and Y is the square root of X
import math
pyDatalog.create_terms(‘math’)
print(X==2) & (Y==math.sqrt(X))

X | Y
–|————–
2 | 1.41421356237

 

‧ 『 == 』是『邏輯謂詞』,其義為『邏輯 is 』。

# give me all the X so that X is 1
print(X==1)

思、學、習其實該三位一體,缺一恐怕『所知』不牢靠,缺兩大概是『不知道』的了。這其中且以『練習』最易為『忽略』,又以『思所學』最難『精通』。故『所謂學』講的是『讀到』文本表達的『實意』,『讀出』字詞背後的『意指』是什麼,方能脈絡貫通 ,義理落實的耶!!

在此僅以一簡單程式作為閱讀 pyDatalog 八皇后問題的梯引︰

 

pi@raspberrypi ~ python3 Python 3.2.3 (default, Mar  1 2013, 11:53:50)  [GCC 4.6.3] on linux2 Type "help", "copyright", "credits" or "license" for more information. >>> from pyDatalog import pyDatalog  >>> pyDatalog.create_terms('解空間, 求解, X, Y')  # 定義 解空間 述詞 一 >>> 解空間(X) <= (X.in_(range(10))) 解空間(X) <= _pyD_in(X,'['0', '1', '2', '3', '4', '5'  # 定義 解空間 述詞 二 >>> 解空間(X, Y) <= 解空間(X) & (Y.in_(range(10))) & (Y == (7 - X)) 解空間(X,Y) <= 解空間(X)&_pyD_in(Y,'['0', '1', '2', '3',  >>> 解空間(X, Y).data [(4, 3), (5, 2), (6, 1), (7, 0), (2, 5), (1, 6), (3, 4), (0, 7)]  # 解空間 引用 >>> 求解(X, Y) <= 解空間(X, Y) & (Y == (X -3)) 求解(X,Y) <= 解空間(X,Y)&==(Y,(X-'3'))  >>> print(求解(X, Y)) X | Y --|-- 5 | 2 >>>  </pre>    <span style="color: #808000;">【範例程式】</span> <pre class="lang:sh decode:true  ">pi@raspberrypi ~ python3
Python 3.2.3 (default, Mar  1 2013, 11:53:50) 
[GCC 4.6.3] on linux2
Type "help", "copyright", "credits" or "license" for more information.
>>> from pyDatalog import pyDatalog
>>> pyDatalog.create_terms('N,X0,X1,X2,X3,X4,X5,X6,X7')
>>> pyDatalog.create_terms('ok,queens,next_queen')

>>> queens(X0)                      <= (X0._in(range(8)))
queens(X0) <= _pyD_in(X0,'['0', '1', '2', '3', '4'
>>> queens(X0,X1)                   <= queens(X0)                   & next_queen(X0,X1)
queens(X0,X1) <= queens(X0)&next_queen(X0,X1)
>>> queens(X0,X1,X2)                <= queens(X0,X1)                & next_queen(X0,X1,X2)
queens(X0,X1,X2) <= queens(X0,X1)&next_queen(X0,X1
>>> queens(X0,X1,X2,X3)             <= queens(X0,X1,X2)             & next_queen(X0,X1,X2,X3)
queens(X0,X1,X2,X3) <= queens(X0,X1,X2)&next_queen
>>> queens(X0,X1,X2,X3,X4)          <= queens(X0,X1,X2,X3)          & next_queen(X0,X1,X2,X3,X4)
queens(X0,X1,X2,X3,X4) <= queens(X0,X1,X2,X3)&next
>>> queens(X0,X1,X2,X3,X4,X5)       <= queens(X0,X1,X2,X3,X4)       & next_queen(X0,X1,X2,X3,X4,X5)
queens(X0,X1,X2,X3,X4,X5) <= queens(X0,X1,X2,X3,X4
>>> queens(X0,X1,X2,X3,X4,X5,X6)    <= queens(X0,X1,X2,X3,X4,X5)    & next_queen(X0,X1,X2,X3,X4,X5,X6)
queens(X0,X1,X2,X3,X4,X5,X6) <= queens(X0,X1,X2,X3
>>> queens(X0,X1,X2,X3,X4,X5,X6,X7) <= queens(X0,X1,X2,X3,X4,X5,X6) & next_queen(X0,X1,X2,X3,X4,X5,X6,X7)
queens(X0,X1,X2,X3,X4,X5,X6,X7) <= queens(X0,X1,X2
>>> next_queen(X0,X1)                   <= queens(X1)                       & ok(X0,1,X1)
next_queen(X0,X1) <= queens(X1)&ok(X0,'1',X1)
>>> next_queen(X0,X1,X2)                <= next_queen(X1,X2)                & ok(X0,2,X2)
next_queen(X0,X1,X2) <= next_queen(X1,X2)&ok(X0,'2
>>> next_queen(X0,X1,X2,X3)             <= next_queen(X1,X2,X3)             & ok(X0,3,X3)
next_queen(X0,X1,X2,X3) <= next_queen(X1,X2,X3)&ok
>>> next_queen(X0,X1,X2,X3,X4)          <= next_queen(X1,X2,X3,X4)          & ok(X0,4,X4)
next_queen(X0,X1,X2,X3,X4) <= next_queen(X1,X2,X3,
>>> next_queen(X0,X1,X2,X3,X4,X5)       <= next_queen(X1,X2,X3,X4,X5)       & ok(X0,5,X5)
next_queen(X0,X1,X2,X3,X4,X5) <= next_queen(X1,X2,
>>> next_queen(X0,X1,X2,X3,X4,X5,X6)    <= next_queen(X1,X2,X3,X4,X5,X6)    & ok(X0,6,X6)
next_queen(X0,X1,X2,X3,X4,X5,X6) <= next_queen(X1,
>>> next_queen(X0,X1,X2,X3,X4,X5,X6,X7) <= next_queen(X1,X2,X3,X4,X5,X6,X7) & ok(X0,7,X7)
next_queen(X0,X1,X2,X3,X4,X5,X6,X7) <= next_queen(
>>> ok(X1, N, X2) <= (X1 != X2) & (X1 != X2+N) & (X1 != X2-N)
ok(X1,N,X2) <= !=(X1,X2)&!=(X1,(X2+N))&!=(X1,(X2-N

>>> print(queens(X0,X1,X2,X3,X4,X5,X6,X7).data[0])
(2, 5, 7, 0, 4, 6, 1, 3)

>>> queens(X0,X1,X2,X3,X4,X5,X6,X7).data
[(5, 2, 0, 7, 3, 1, 6, 4), (5, 1, 6, 0, 3, 7, 4, 2), (4, 7, 3, 0, 2, 5, 1, 6), (3, 1, 7, 5, 0, 2, 4, 6), (3, 0, 4, 7, 5, 2, 6, 1), (6, 3, 1, 7, 5, 0, 2, 4), (6, 1, 3, 0, 7, 4, 2, 5), (3, 1, 6, 2, 5, 7, 0, 4), (3, 5, 7, 1, 6, 0, 2, 4), (3, 6, 0, 7, 4, 1, 5, 2), (2, 4, 1, 7, 5, 3, 6, 0), (6, 2, 0, 5, 7, 4, 1, 3), (3, 7, 0, 4, 6, 1, 5, 2), (7, 1, 3, 0, 6, 4, 2, 5), (4, 0, 7, 5, 2, 6, 1, 3), (2, 5, 1, 6, 4, 0, 7, 3), (5, 2, 6, 3, 0, 7, 1, 4), (2, 5, 1, 6, 0, 3, 7, 4), (4, 6, 3, 0, 2, 7, 5, 1), (7, 1, 4, 2, 0, 6, 3, 5), (1, 6, 2, 5, 7, 4, 0, 3), (6, 1, 5, 2, 0, 3, 7, 4), (4, 2, 7, 3, 6, 0, 5, 1), (3, 7, 4, 2, 0, 6, 1, 5), (4, 1, 7, 0, 3, 6, 2, 5), (5, 7, 1, 3, 0, 6, 4, 2), (5, 3, 0, 4, 7, 1, 6, 2), (2, 5, 7, 1, 3, 0, 6, 4), (3, 6, 4, 1, 5, 0, 2, 7), (5, 3, 1, 7, 4, 6, 0, 2), (4, 2, 0, 5, 7, 1, 3, 6), (6, 4, 2, 0, 5, 7, 1, 3), (3, 0, 4, 7, 1, 6, 2, 5), (5, 2, 6, 1, 7, 4, 0, 3), (6, 0, 2, 7, 5, 3, 1, 4), (2, 6, 1, 7, 4, 0, 3, 5), (5, 1, 6, 0, 2, 4, 7, 3), (3, 6, 2, 7, 1, 4, 0, 5), (4, 1, 3, 6, 2, 7, 5, 0), (5, 2, 6, 1, 3, 7, 0, 4), (2, 0, 6, 4, 7, 1, 3, 5), (3, 1, 6, 2, 5, 7, 4, 0), (4, 6, 1, 5, 2, 0, 3, 7), (1, 6, 4, 7, 0, 3, 5, 2), (2, 4, 1, 7, 0, 6, 3, 5), (3, 1, 4, 7, 5, 0, 2, 6), (2, 4, 7, 3, 0, 6, 1, 5), (4, 6, 0, 3, 1, 7, 5, 2), (1, 4, 6, 0, 2, 7, 5, 3), (5, 0, 4, 1, 7, 2, 6, 3), (3, 7, 0, 2, 5, 1, 6, 4), (5, 3, 6, 0, 7, 1, 4, 2), (1, 3, 5, 7, 2, 0, 6, 4), (7, 2, 0, 5, 1, 4, 6, 3), (7, 3, 0, 2, 5, 1, 6, 4), (2, 5, 7, 0, 3, 6, 4, 1), (5, 2, 4, 7, 0, 3, 1, 6), (2, 6, 1, 7, 5, 3, 0, 4), (4, 6, 1, 3, 7, 0, 2, 5), (3, 6, 4, 2, 0, 5, 7, 1), (5, 2, 0, 7, 4, 1, 3, 6), (6, 2, 7, 1, 4, 0, 5, 3), (0, 4, 7, 5, 2, 6, 1, 3), (5, 2, 0, 6, 4, 7, 1, 3), (1, 4, 6, 3, 0, 7, 5, 2), (4, 7, 3, 0, 6, 1, 5, 2), (4, 1, 3, 5, 7, 2, 0, 6), (1, 5, 0, 6, 3, 7, 2, 4), (0, 6, 3, 5, 7, 1, 4, 2), (5, 3, 6, 0, 2, 4, 1, 7), (6, 3, 1, 4, 7, 0, 2, 5), (1, 5, 7, 2, 0, 3, 6, 4), (5, 2, 4, 6, 0, 3, 1, 7), (2, 7, 3, 6, 0, 5, 1, 4), (0, 6, 4, 7, 1, 3, 5, 2), (3, 1, 6, 4, 0, 7, 5, 2), (2, 5, 3, 1, 7, 4, 6, 0), (1, 7, 5, 0, 2, 4, 6, 3), (4, 6, 1, 5, 2, 0, 7, 3), (3, 1, 7, 4, 6, 0, 2, 5), (3, 5, 0, 4, 1, 7, 2, 6), (2, 5, 1, 4, 7, 0, 6, 3), (4, 1, 5, 0, 6, 3, 7, 2), (4, 0, 3, 5, 7, 1, 6, 2), (2, 5, 3, 0, 7, 4, 6, 1), (0, 5, 7, 2, 6, 3, 1, 4), (4, 2, 0, 6, 1, 7, 5, 3), (4, 6, 0, 2, 7, 5, 3, 1), (3, 5, 7, 2, 0, 6, 4, 1), (2, 4, 6, 0, 3, 1, 7, 5), (2, 5, 7, 0, 4, 6, 1, 3), (4, 0, 7, 3, 1, 6, 2, 5)]

>>> len(queens(X0,X1,X2,X3,X4,X5,X6,X7).data)
92
>>> 

 

N 皇后範例︰

pyDatalog / pyDatalog / examples / queens_N.py