【形式化方法】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形式化課程筆記-歡迎留言與私信交流

#隨手點贊，我會更開心~~^_^