【形式化方法】PartB:LA/LP Applications(N皇后问题)

2023-11-20 16:10

本文主要是介绍【形式化方法】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 boardfor 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 = 0dia = []anti_dia = []# 对角线元素放到dia数组里面for row in board:j = 0for pos in row:if i == j:dia.append(pos)j = j + 1i = i + 1solver.add(sum(dia) <= 1)    # 约束3:对角线最多只有一个皇后# print(dia)# 反对角线元素放到anti_dia数组里面i = 0for row in board:j = 0for pos in row:if i + j == n-1 :anti_dia.append(pos)j = j + 1i = i + 1# print(anti_dia)solver.add(sum(anti_dia) <= 1)  # 约束4:反对角线最多只有一个皇后# count the number of solutionssolution_count = 0start = time.time()while solver.check() == sat:solution_count += 1model = solver.model()if verbose:# print the solutionprint([(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 solutionsolution_cons = [(flag == 1) for row in board for flag in row if model[flag] == 1]# add solution to the solver to get new solutionsolver.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_sizesolutions = [[]]def is_safe(col, solution):same_col = col in solutionsame_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 solutionsfor 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 columnsolver.add([Distinct(queens)])# at most one for per anti-diagonal & diagonalsolver.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 solutionssolution_count = 0start = time.time()while solver.check() == sat:solution_count += 1model = solver.model()if verbose:# print the solutionsprint([(index, model[queen]) for index, queen in enumerate(queens)])# generate constraints from solutionsolution_cons = [(queen == model[queen]) for queen in queens]# add solution to the solver to get new solutionsolver.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形式化课程笔记-欢迎留言与私信交流

#随手点赞,我会更开心~~^_^

 

 

这篇关于【形式化方法】PartB:LA/LP Applications(N皇后问题)的文章就介绍到这儿,希望我们推荐的文章对编程师们有所帮助!



http://www.chinasem.cn/article/395837

相关文章

Conda与Python venv虚拟环境的区别与使用方法详解

《Conda与Pythonvenv虚拟环境的区别与使用方法详解》随着Python社区的成长,虚拟环境的概念和技术也在不断发展,:本文主要介绍Conda与Pythonvenv虚拟环境的区别与使用... 目录前言一、Conda 与 python venv 的核心区别1. Conda 的特点2. Python v

Spring Boot中WebSocket常用使用方法详解

《SpringBoot中WebSocket常用使用方法详解》本文从WebSocket的基础概念出发,详细介绍了SpringBoot集成WebSocket的步骤,并重点讲解了常用的使用方法,包括简单消... 目录一、WebSocket基础概念1.1 什么是WebSocket1.2 WebSocket与HTTP

SQL Server配置管理器无法打开的四种解决方法

《SQLServer配置管理器无法打开的四种解决方法》本文总结了SQLServer配置管理器无法打开的四种解决方法,文中通过图文示例介绍的非常详细,对大家的学习或者工作具有一定的参考学习价值,需要的... 目录方法一:桌面图标进入方法二:运行窗口进入检查版本号对照表php方法三:查找文件路径方法四:检查 S

MyBatis-Plus 中 nested() 与 and() 方法详解(最佳实践场景)

《MyBatis-Plus中nested()与and()方法详解(最佳实践场景)》在MyBatis-Plus的条件构造器中,nested()和and()都是用于构建复杂查询条件的关键方法,但... 目录MyBATis-Plus 中nested()与and()方法详解一、核心区别对比二、方法详解1.and()

golang中reflect包的常用方法

《golang中reflect包的常用方法》Go反射reflect包提供类型和值方法,用于获取类型信息、访问字段、调用方法等,文中通过示例代码介绍的非常详细,对大家的学习或者工作具有一定的参考学习价值... 目录reflect包方法总结类型 (Type) 方法值 (Value) 方法reflect包方法总结

C# 比较两个list 之间元素差异的常用方法

《C#比较两个list之间元素差异的常用方法》:本文主要介绍C#比较两个list之间元素差异,本文通过实例代码给大家介绍的非常详细,对大家的学习或工作具有一定的参考借鉴价值,需要的朋友参考下吧... 目录1. 使用Except方法2. 使用Except的逆操作3. 使用LINQ的Join,GroupJoin

怎样通过分析GC日志来定位Java进程的内存问题

《怎样通过分析GC日志来定位Java进程的内存问题》:本文主要介绍怎样通过分析GC日志来定位Java进程的内存问题,具有很好的参考价值,希望对大家有所帮助,如有错误或未考虑完全的地方,望不吝赐教... 目录一、GC 日志基础配置1. 启用详细 GC 日志2. 不同收集器的日志格式二、关键指标与分析维度1.

MySQL查询JSON数组字段包含特定字符串的方法

《MySQL查询JSON数组字段包含特定字符串的方法》在MySQL数据库中,当某个字段存储的是JSON数组,需要查询数组中包含特定字符串的记录时传统的LIKE语句无法直接使用,下面小编就为大家介绍两种... 目录问题背景解决方案对比1. 精确匹配方案(推荐)2. 模糊匹配方案参数化查询示例使用场景建议性能优

Java 线程安全与 volatile与单例模式问题及解决方案

《Java线程安全与volatile与单例模式问题及解决方案》文章主要讲解线程安全问题的五个成因(调度随机、变量修改、非原子操作、内存可见性、指令重排序)及解决方案,强调使用volatile关键字... 目录什么是线程安全线程安全问题的产生与解决方案线程的调度是随机的多个线程对同一个变量进行修改线程的修改操

关于集合与数组转换实现方法

《关于集合与数组转换实现方法》:本文主要介绍关于集合与数组转换实现方法,具有很好的参考价值,希望对大家有所帮助,如有错误或未考虑完全的地方,望不吝赐教... 目录1、Arrays.asList()1.1、方法作用1.2、内部实现1.3、修改元素的影响1.4、注意事项2、list.toArray()2.1、方