【形式化方法】PartB:LA/LP Applications(N皇后問題)
N-Queen Problem:
在作業3(挑戰問題)中,我們在SAT之前解決了N個皇后的問題(4個皇后)。這個問題是關於把N個皇后放在一個N*N的棋盤上,這樣就沒有兩個皇后互相威脅了。一種解決方案要求沒有兩個皇后共享同一行、列、對角線或反對角線。下圖顯示了N = 4的樣本N -皇后謎題的解:
這個問題的目標是在一個N*N棋盤,找出存在多少個解。
SAT實現的基本思想是通過Bool值構造n-queen謎題約束。實際上,我們可以用LA來求解n-queen問題,它比SAT更容易理解,也更高效。其思路與求解子集和問題的思路相同。我們使用一個二維的0-1標誌F來代表棋盤的每個單元格,F有值:
滿足 0 < i <N, 0< j < N 。我們可以建立n-queen謎題的約束條件如下:
- 每一行只有一個皇后: 0< i <N
- 每一列只有一個皇后:0 < j < N
- 每條對角線最多有1個皇后:-N < d < N
- 每條反對角線最多有1個皇后: 0 < d < 2N -1
Exercise 11: 閱讀queen.py Python檔案中的程式碼,完成n_queen_la()方法,該方法使用0-1 ILA解決n-queen問題。您可以通過參考我們上面討論的模型來構造約束,或者您可以提出您自己的約束。
# LA演算法解決N皇后問題 def n_queen_la(board_size: int, verbose: bool = False) -> int: solver = Solver() n = board_size # Each position of the board is represented by a 0-1 integer variable: # ... ... ... ... # x_2_0 x_2_1 x_2_2 ... # x_1_0 x_1_1 x_1_2 ... # x_0_0 x_0_1 x_0_2 ... # board = [[Int(f"x_{row}_{col}") for col in range(n)] for row in range(n)] # only be 0 or 1 in board for row in board: for pos in row: solver.add(Or(pos == 0, pos == 1)) # print(row) # @exercise 11: please fill in the missing code to add # the following constraint into the solver: # each row has just 1 queen, # each column has just 1 queen, # each diagonal has at most 1 queen, # each anti-diagonal has at most 1 queen. # raise Todo("exercise 11: please fill in the missing code.") for row in board: # print(row) solver.add(sum(row) == 1) # 約束1:一行只有一個皇后 for col in board: # print(col) solver.add(sum(col) == 1) # 約束2: 一列只有一個皇后 i = 0 dia = [] anti_dia = [] # 對角線元素放到dia數組裡面 for row in board: j = 0 for pos in row: if i == j: dia.append(pos) j = j + 1 i = i + 1 solver.add(sum(dia) <= 1) # 約束3:對角線最多隻有一個皇后 # print(dia) # 反對角線元素放到anti_dia數組裡面 i = 0 for row in board: j = 0 for pos in row: if i + j == n-1 : anti_dia.append(pos) j = j + 1 i = i + 1 # print(anti_dia) solver.add(sum(anti_dia) <= 1) # 約束4:反對角線最多隻有一個皇后 # count the number of solutions solution_count = 0 start = time.time() while solver.check() == sat: solution_count += 1 model = solver.model() if verbose: # print the solution print([(row_index, col_index) for row_index, row in enumerate(board) for col_index, flag in enumerate(row) if model[flag] == 1]) # generate constraints from solution solution_cons = [(flag == 1) for row in board for flag in row if model[flag] == 1] # add solution to the solver to get new solution solver.add(Not(And(solution_cons))) print(f"n_queen_la solve {board_size}-queens by {(time.time() - start):.6f}s") return solution_count
另一種解決N -queen問題的方法是使用回溯演算法,但複雜度相對於棋盤大小N是指數級的。
Exercise 12:queen.py Python檔案中的程式碼,在n_queen_bt()方法中有一個基於回溯的解決方案。嘗試比較回溯演算法和LA演算法,通過改變棋盤大小N的值為其他值,哪一個更快?從結果中你能得出什麼結論?
#回溯法解決N皇后問題 def n_queen_bt(board_size: int, verbose: bool = False) -> int: n = board_size solutions = [[]] def is_safe(col, solution): same_col = col in solution same_diag = any(abs(col - j) == (len(solution) - i) for i, j in enumerate(solution)) return not (same_col or same_diag) start = time.time() for row in range(n): solutions = [solution + [col] for solution in solutions for col in range(n) if is_safe(col, solution)] print(f"n_queen_bt solve {board_size}-queens by {(time.time() - start):.6f}s") if verbose: # print the solutions for solution in solutions: print(list(enumerate(solution))) return len(solutions)
上述LA實現並不是求解n-queen問題的唯一演算法。事實上,我們建立約束來描述問題的方式往往對演算法的效率有很大的影響。
Exercise 13: 閱讀queen.py Python檔案中n_queen_la_opt()方法的程式碼。試著將此方法的效率與練習11中的實現進行比較。你的觀察是什麼?你能得出什麼結論?
# LA優化演算法解決N皇后問題
def n_queen_la_opt(board_size: int, verbose: bool = False) -> int:
solver = Solver()
n = board_size
# We know each queen must be in a different row.
# So, we represent each queen by a single integer: the column position
# the q_i = j means queen in the row i and column j.
queens = [Int(f"q_{i}") for i in range(n)]
# each queen is in a column {0, ... 7 }
solver.add([And(0 <= queens[i], queens[i] < n) for i in range(n)])
# one queen per column
solver.add([Distinct(queens)])
# at most one for per anti-diagonal & diagonal
solver.add([If(i == j, True, And(queens[i] - queens[j] != i - j, queens[i] - queens[j] != j - i))
for i in range(n) for j in range(i)])
# count the number of solutions
solution_count = 0
start = time.time()
while solver.check() == sat:
solution_count += 1
model = solver.model()
if verbose:
# print the solutions
print([(index, model[queen]) for index, queen in enumerate(queens)])
# generate constraints from solution
solution_cons = [(queen == model[queen]) for queen in queens]
# add solution to the solver to get new solution
solver.add(Not(And(solution_cons)))
print(f"n_queen_la_opt solve {board_size}-queens by {(time.time() - start):.6f}s")
return solution_count
N = 4時,比較執行時間:
N = 5 時,比較執行時間:
結論:
三種演算法解決N皇后問題效率的比較: 用回溯法最快、LA優化演算法其次、LA演算法最慢
#中科大軟院-hbj形式化課程筆記-歡迎留言與私信交流
#隨手點贊,我會更開心~~^_^