【形式化方法】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

相关文章

好题——hdu2522(小数问题:求1/n的第一个循环节)

好喜欢这题,第一次做小数问题,一开始真心没思路,然后参考了网上的一些资料。 知识点***********************************无限不循环小数即无理数,不能写作两整数之比*****************************(一开始没想到,小学没学好) 此题1/n肯定是一个有限循环小数,了解这些后就能做此题了。 按照除法的机制,用一个函数表示出来就可以了,代码如下

hdu1043(八数码问题,广搜 + hash(实现状态压缩) )

利用康拓展开将一个排列映射成一个自然数,然后就变成了普通的广搜题。 #include<iostream>#include<algorithm>#include<string>#include<stack>#include<queue>#include<map>#include<stdio.h>#include<stdlib.h>#include<ctype.h>#inclu

【C++】_list常用方法解析及模拟实现

相信自己的力量,只要对自己始终保持信心,尽自己最大努力去完成任何事,就算事情最终结果是失败了,努力了也不留遗憾。💓💓💓 目录   ✨说在前面 🍋知识点一:什么是list? •🌰1.list的定义 •🌰2.list的基本特性 •🌰3.常用接口介绍 🍋知识点二:list常用接口 •🌰1.默认成员函数 🔥构造函数(⭐) 🔥析构函数 •🌰2.list对象

浅谈主机加固,六种有效的主机加固方法

在数字化时代,数据的价值不言而喻,但随之而来的安全威胁也日益严峻。从勒索病毒到内部泄露,企业的数据安全面临着前所未有的挑战。为了应对这些挑战,一种全新的主机加固解决方案应运而生。 MCK主机加固解决方案,采用先进的安全容器中间件技术,构建起一套内核级的纵深立体防护体系。这一体系突破了传统安全防护的局限,即使在管理员权限被恶意利用的情况下,也能确保服务器的安全稳定运行。 普适主机加固措施:

购买磨轮平衡机时应该注意什么问题和技巧

在购买磨轮平衡机时,您应该注意以下几个关键点: 平衡精度 平衡精度是衡量平衡机性能的核心指标,直接影响到不平衡量的检测与校准的准确性,从而决定磨轮的振动和噪声水平。高精度的平衡机能显著减少振动和噪声,提高磨削加工的精度。 转速范围 宽广的转速范围意味着平衡机能够处理更多种类的磨轮,适应不同的工作条件和规格要求。 振动监测能力 振动监测能力是评估平衡机性能的重要因素。通过传感器实时监

webm怎么转换成mp4?这几种方法超多人在用!

webm怎么转换成mp4?WebM作为一种新兴的视频编码格式,近年来逐渐进入大众视野,其背后承载着诸多优势,但同时也伴随着不容忽视的局限性,首要挑战在于其兼容性边界,尽管WebM已广泛适应于众多网站与软件平台,但在特定应用环境或老旧设备上,其兼容难题依旧凸显,为用户体验带来不便,再者,WebM格式的非普适性也体现在编辑流程上,由于它并非行业内的通用标准,编辑过程中可能会遭遇格式不兼容的障碍,导致操

透彻!驯服大型语言模型(LLMs)的五种方法,及具体方法选择思路

引言 随着时间的发展,大型语言模型不再停留在演示阶段而是逐步面向生产系统的应用,随着人们期望的不断增加,目标也发生了巨大的变化。在短短的几个月的时间里,人们对大模型的认识已经从对其zero-shot能力感到惊讶,转变为考虑改进模型质量、提高模型可用性。 「大语言模型(LLMs)其实就是利用高容量的模型架构(例如Transformer)对海量的、多种多样的数据分布进行建模得到,它包含了大量的先验

缓存雪崩问题

缓存雪崩是缓存中大量key失效后当高并发到来时导致大量请求到数据库,瞬间耗尽数据库资源,导致数据库无法使用。 解决方案: 1、使用锁进行控制 2、对同一类型信息的key设置不同的过期时间 3、缓存预热 1. 什么是缓存雪崩 缓存雪崩是指在短时间内,大量缓存数据同时失效,导致所有请求直接涌向数据库,瞬间增加数据库的负载压力,可能导致数据库性能下降甚至崩溃。这种情况往往发生在缓存中大量 k

6.1.数据结构-c/c++堆详解下篇(堆排序,TopK问题)

上篇:6.1.数据结构-c/c++模拟实现堆上篇(向下,上调整算法,建堆,增删数据)-CSDN博客 本章重点 1.使用堆来完成堆排序 2.使用堆解决TopK问题 目录 一.堆排序 1.1 思路 1.2 代码 1.3 简单测试 二.TopK问题 2.1 思路(求最小): 2.2 C语言代码(手写堆) 2.3 C++代码(使用优先级队列 priority_queue)

【北交大信息所AI-Max2】使用方法

BJTU信息所集群AI_MAX2使用方法 使用的前提是预约到相应的算力卡,拥有登录权限的账号密码,一般为导师组共用一个。 有浏览器、ssh工具就可以。 1.新建集群Terminal 浏览器登陆10.126.62.75 (如果是1集群把75改成66) 交互式开发 执行器选Terminal 密码随便设一个(需记住) 工作空间:私有数据、全部文件 加速器选GeForce_RTX_2080_Ti