求解恰当可满足性问题的随机局部搜索算法

doi:10.11772/j.issn.1001-9081.2023030364

《计算机应用》唯一官方网站 ›› 2024, Vol. 44 ›› Issue (3): 842-848.DOI: 10.11772/j.issn.1001-9081.2023030364

求解恰当可满足性问题的随机局部搜索算法

赵星宇¹, 王晓峰¹^,²(), 杨易¹, 庞立超¹, 杨澜¹

^1.北方民族大学计算机科学与工程学院，银川 750021
^2.图像图形智能处理国家民委重点实验室（北方民族大学），银川 750021

收稿日期:2023-04-04 修回日期:2023-04-26 接受日期:2023-05-04 发布日期:2023-05-18 出版日期:2024-03-10
通讯作者: 王晓峰
作者简介:赵星宇（1999—），男，湖北荆州人，硕士研究生，CCF会员，主要研究方向：算法分析与设计
杨易（1995—），男，陕西咸阳人，硕士研究生，CCF会员，主要研究方向：算法分析与设计
庞立超（1993—），男，山东临沂人，硕士研究生，CCF会员，主要研究方向：算法分析与设计
杨澜（1997—），女，山西忻州人，硕士研究生，CCF会员，主要研究方向：算法分析与设计。
基金资助:
国家自然科学基金资助项目(62062001);宁夏青年拔尖人才项目(2021)

Stochastic local search algorithm for solving exact satisfiability problem

Xingyu ZHAO¹, Xiaofeng WANG¹^,²(), Yi YANG¹, Lichao PANG¹, Lan YANG¹

^1.School of Computer Science and Engineering，North Minzu University，Yinchuan Ningxia 750021，China
^2.Key Laboratory of Images & Graphics Intelligent Processing of State Ethnic Affairs Commission （North Minzu University），Yinchuan Ningxia 750021，China

Received:2023-04-04 Revised:2023-04-26 Accepted:2023-05-04 Online:2023-05-18 Published:2024-03-10
Contact: Xiaofeng WANG
About author:ZHAO Xingyu， born in 1999， M. S. candidate. His research interests include algorithm analysis and design.
YANG Yi， born in 1995， M. S. candidate. His research interests include algorithm analysis and design.
PANG Lichao， born in 1993， M. S. candidate. His research interests include algorithm analysis and design.
YANG Lan， born in 1997， M. S. candidate. Her research interests include algorithm analysis and design.
Supported by:
National Natural Science Foundation of China(62062001);Ningxia Youth Top Talent Project(2021)

摘要/Abstract

摘要：

可满足性问题（SAT）是一种NP完全问题，被广泛运用于人工智能和机器学习等研究。恰当可满足性问题（XSAT）是SAT中一类重要的子问题。目前的大部分关于XSAT的研究主要为理论层面，对高效的求解算法特别是具有高效验证性的随机局部搜索算法研究很少。针对以上问题，分析了基础编码和等价编码两种转化方式的公式的部分性质，提出一种直接求解XSAT的随机局部搜索算法WalkXSAT。首先使用随机局部搜索框架进行基础搜索与条件判定；其次加入变元所属文字的恰当不可满足计分值，优先处理不易恰当满足的变元；然后使用防重复选择翻转变元的启发式策略减小搜索空间；最后，采用多种来源以及多种格式的实例进行对比实验。在直接求解XSAT时，相较于ProbSAT，WalkXSAT的变元翻转次数与求解时间显著减少；在求解基础编码转化后的实例中，当实例变元规模大于100时，ProbSAT已失效，而WalkXSAT依然能够在短时间内求解。实验结果表明，所提WalkXSAT精确性高、稳定性强、收敛快。

关键词: 随机局部搜索算法, 恰当可满足性问题, 可满足性问题, 基础编码, 等价编码

Abstract:

SATisfiability problem （SAT） is a NP complete problem， which is widely used in artificial intelligence and machine learning. Exact SATisfiability problem （XSAT） is an important subproblem of SAT. Most of the current research on XSAT is mainly at the theoretical level， but few efficient solution algorithms are studied， especially the stochastic local search algorithms with efficient verifiability. To address above problems and analyze some properties of both basic and equivalent coding formulas， a stochastic local search algorithm WalkXSAT was proposed for solving XSAT directly. Firstly， the random local search framework was used for basic search and condition determination. Secondly， the appropriate unsatisfiable scoring value of the text to which the variables belonged was added， and the variables that were not easily and appropriately satisfied were prioritized. Thirdly， the search space was reduced using the heuristic strategy of anti-repeat selection of flipped variables. Finally， multiple sources and multiple formats of examples were used for comparison experiments. Compared with ProbSAT algorithm， the number variable flips and the solving time of WalkXSAT are significantly reduced when directly solving the XSAT. In the example after solving the basic encoding transformation， when the variable size of the example is greater than 100， the ProbSAT algorithm is no longer effective， while WalkXSAT can still solve the XSAT in a short time. Experimental results show that the proposed algorithm WalkXSAT has high accuracy， strong stability， and fast convergence speed.

Key words: stochastic local search algorithm, Exact SATisfiability problem (XSAT), SATisfiability problem (SAT), basic encoding, equivalent encoding

中图分类号:

TP301

赵星宇, 王晓峰, 杨易, 庞立超, 杨澜. 求解恰当可满足性问题的随机局部搜索算法[J]. 计算机应用, 2024, 44(3): 842-848.

Xingyu ZHAO, Xiaofeng WANG, Yi YANG, Lichao PANG, Lan YANG. Stochastic local search algorithm for solving exact satisfiability problem[J]. Journal of Computer Applications, 2024, 44(3): 842-848.

图/表 5

参考文献 21

1	TOVEY C A. A simplified NP-complete satisfiability problem ［J］. Discrete Applied Mathematics， 1984， 8（1）： 85-89. 10.1016/0166-218x(84)90081-7
2	SCHNEIDER S， BURGHOLZER L， WILLE R. A SAT encoding for optimal Clifford circuit synthesis ［C］// Proceedings of the 28th Asia and South Pacific Design Automation Conference. New York： ACM， 2023： 190-195. 10.1145/3566097.3567929
3	KANG M， LI Y， JIAO L， et al. Differential analysis of ARX block ciphers based on an improved genetic algorithm ［J］. Chinese Journal of Electronics， 2023， 32（2）： 225-236. 10.23919/cje.2021.00.415
4	LI J， HAN D， WU Z， et al. A novel system for medical equipment supply chain traceability based on alliance chain and attribute and role access control ［J］. Future Generation Computer Systems， 2023， 142： 195-211. 10.1016/j.future.2022.12.037
5	BRESLER G， HUANG B. The algorithmic phase transition of random kSAT for low degree polynomials ［C］// Proceedings of the IEEE 62nd Annual Symposium on Foundations of Computer Science. Piscataway： IEEE， 2022： 298-309. 10.1109/focs52979.2021.00038
6	AL-YAHYA T， MENAI M E B A， MATHKOUR H. Boosting the performance of CDCL-based SAT solvers by exploiting backbones and backdoors ［J］. Algorithms， 2022， 15（9）： No.302. 10.3390/a15090302
7	ALYAHYA T N， MENAI M E B， MATHKOUR H. On the structure of the Boolean satisfiability problem： a survey ［J］. ACM Computing Surveys， 2022， 55（3）： No.46. 10.1145/3491210
8	NOGUCHI T， FUJIWARA A. An asynchronous P system with a DPLL algorithm for solving SAT ［J］. International Journal of Networking and Computing， 2022， 12（2）： 238-252. 10.15803/ijnc.12.2_238
9	LUO M， LI C-M， XIAO F， et al. An effective learnt clause minimization approach for CDCL SAT solvers ［C］// Proceedings of the 26th International Joint Conference on Artificial Intelligence. New York： ACM， 2017： 703-711. 10.24963/ijcai.2017/98
10	HIRECHE C， DRIAS H， MOULAI H. Grid based clustering for satisfiability solving ［J］. Applied Soft Computing， 2020， 88： 106069. 10.1016/j.asoc.2020.106069
11	FU H， XU Y， CHEN S， et al. Improving WalkSAT for random 3-SAT problems ［J］. Journal of Universal Computer Science， 2020， 26（2）： 220-243. 10.3897/jucs.2020.013
12	VARMANTCHAONALA C M， FENDJI J L K E， NJAFA J P T， et al. Quantum hybrid algorithm for solving SAT problem ［J］. Engineering Applications of Artificial Intelligence， 2023， 121： 106058. 10.1016/j.engappai.2023.106058
13	BALYO T， CHRPA L. Using algorithm configuration tools to generate hard SAT benchmarks ［C］// Proceedings of the 11th International Symposium on Combinatorial Search. Menlo Park， CA： AAAI Press， 2018： 133-137.
14	BYSKOV J M， MADSEN B A， SKJERNAA B. New algorithms for exact satisfiability ［J］. Theoretical Computer Science， 2005， 332（1/2/3）： 515-541. 10.1016/j.tcs.2004.12.023
15	王晓峰，于卓，周锦程，等.随机均衡正则恰当（2s，k）-SAT问题的可满足相变［J］.华中科技大学学报（自然科学版）， 2022， 50（2）： 105-111.
	WANG X F， YU Z， ZHOU J C， et al. Phase transition of in random balance regular exact（2s，k）-SAT problem ［J］. Journal of Huazhong University of Science and Technology （Natural Science Edition）， 2022，50（2）：105-111.
16	周俊萍，姜蕴晖，殷明浩.最坏情况下X2SAT问题的上界［J］.计算机研究与发展，2014，51（3）：598-605. 10.7544/issn1000-1239.2014.20120587
	ZHOU J P， JIANG Y H， YIN M H. New worst-case upper bounds for X2SAT ［J］. Journal of Computer Research and Development， 2014，51（3）：598-605. 10.7544/issn1000-1239.2014.20120587
17	OSTROWSKI R， PARIS L. From XSAT to SAT by exhibiting equivalencies ［C］// Proceedings of the 20th IEEE International Conference on Tools with Artificial Intelligence. Piscataway： IEEE， 2008： 84-91. 10.1109/ictai.2008.80
18	FANG C L， LIU J. A linear algebra formulation for boolean satisfiability testing ［EB/OL］. ［2023-01-23］. .
19	LIU J， ZHOU H. A development of LAF for satisfying assignments search ［C］// Proceedings of the IEEE 3rd Information Technology， Networking， Electronic and Automation Control Conference. Piscataway： IEEE， 2019： 719-726. 10.1109/itnec.2019.8729332
20	BALINT A， SCHÖNING U. Choosing probability distributions for stochastic local search and the role of make versus break ［C］// Proceedings of 15th International Conference on Theory and Applications of Satisfiability Testing. Berlin： Springer， 2012： 16-29. 10.1007/978-3-642-31612-8_3
21	CAI S， SU K. Configuration checking with aspiration in local search for SAT ［C］// Proceedings of the 26th AAAI Conference on Artificial Intelligence. Menlo Park， CA： AAAI Press， 2012： 434-440.

实验序号	实例类型	变元数	子句数	子句变元比	算法	成功率/%	平均翻转次数	标准差	平均运行时间/s
1	3CNF	20	10	0.50	WX	100	23.8	17.16	0.001 6
					BF	100	—	—	1.606 2
					PS	100	455.9	312.69	0.060 5
2	3CNF	20	15	0.75	WX	100	65.7	19.09	0.004 2
					BF	100	—	—	1.597 8
					PS	100	247.7	182.51	0.042 9
3	3CNF	20	20	1.00	WX	100	79.1	60.39	0.004 1
					BF	100	—	—	1.613 0
					PS	100	146.3	129.02	0.034 4
4	3CNF	100	50	0.50	WX	100	1 020.0	986.62	0.104 2
					BF	0	—	—	—
					PS	90	71 297.0	48 326.28	45.673 3
5	3CNF	100	65	0.65	WX	100	1 657.8	1 276.61	0.164 0
					BF	0	—	—	—
					PS	80	35 755.6	19 519.40	28.546 3
6	4CNF	20	10	0.50	WX	100	139.3	69.41	0.005 0
					BF	100	—	—	2.065 4
					PS	100	1 104.9	749.39	0.249 4
7	4CNF	20	15	0.75	WX	100	103.7	63.31	0.004 4
					BF	100	—	—	1.479 1
					PS	100	106.5	103.04	0.033 4
8	4CNF	50	25	0.50	WX	100	538.9	280.97	0.025 5
					BF	0	—	—	—
					PS	100	2 613.4	2 789.73	1.475 0
9	4CNF	50	30	0.60	WX	100	1 640.7	1 882.03	0.101 4
					BF	0	—	—	—
					PS	100	3 750.1	4 009.83	1.795 8
10	4-（2s，k）-CNF	20	10	0.50	WX	100	82.8	45.74	0.004 2
					BF	100	—	—	1.617 0
					PS	100	592.1	644.19	0.088 2
11	4-（2s，k）-CNF	50	25	0.50	WX	100	493.4	244.03	0.035 3
					BF	0	—	—	—
					PS	100	5 956.2	3 481.37	2.920 8
12	网络容错（2-4）CNF	1 283	523	0.40	WX	100	5 229.5	1 086.28	3. 7 172
					BF	0	—	—	—
					PS	0	—	—	—
13	网络容错（3-4）CNF	1 516	645	0.42	WX	100	9 272.0	3 179.17	8.328 6
					BF	0	—	—	—
					PS	0	—	—	—

实验序号	实例类型	变元数	子句数	子句变元比	算法	成功率/%	平均翻转次数	标准差	平均运行时间/s
1	3CNF	20	10	0.50	WX	100	23.8	17.16	0.001 6
					BF	100	—	—	1.606 2
					PS	100	455.9	312.69	0.060 5
2	3CNF	20	15	0.75	WX	100	65.7	19.09	0.004 2
					BF	100	—	—	1.597 8
					PS	100	247.7	182.51	0.042 9
3	3CNF	20	20	1.00	WX	100	79.1	60.39	0.004 1
					BF	100	—	—	1.613 0
					PS	100	146.3	129.02	0.034 4
4	3CNF	100	50	0.50	WX	100	1 020.0	986.62	0.104 2
					BF	0	—	—	—
					PS	90	71 297.0	48 326.28	45.673 3
5	3CNF	100	65	0.65	WX	100	1 657.8	1 276.61	0.164 0
					BF	0	—	—	—
					PS	80	35 755.6	19 519.40	28.546 3
6	4CNF	20	10	0.50	WX	100	139.3	69.41	0.005 0
					BF	100	—	—	2.065 4
					PS	100	1 104.9	749.39	0.249 4
7	4CNF	20	15	0.75	WX	100	103.7	63.31	0.004 4
					BF	100	—	—	1.479 1
					PS	100	106.5	103.04	0.033 4
8	4CNF	50	25	0.50	WX	100	538.9	280.97	0.025 5
					BF	0	—	—	—
					PS	100	2 613.4	2 789.73	1.475 0
9	4CNF	50	30	0.60	WX	100	1 640.7	1 882.03	0.101 4
					BF	0	—	—	—
					PS	100	3 750.1	4 009.83	1.795 8
10	4-（2s，k）-CNF	20	10	0.50	WX	100	82.8	45.74	0.004 2
					BF	100	—	—	1.617 0
					PS	100	592.1	644.19	0.088 2
11	4-（2s，k）-CNF	50	25	0.50	WX	100	493.4	244.03	0.035 3
					BF	0	—	—	—
					PS	100	5 956.2	3 481.37	2.920 8
12	网络容错（2-4）CNF	1 283	523	0.40	WX	100	5 229.5	1 086.28	3. 7 172
					BF	0	—	—	—
					PS	0	—	—	—
13	网络容错（3-4）CNF	1 516	645	0.42	WX	100	9 272.0	3 179.17	8.328 6
					BF	0	—	—	—
					PS	0	—	—	—

实验序号	算法	平均翻转次数	标准差	平均运行时间/s
1	WX	23.5	10.76	0.002 6
1	PS	16.3	11.69	0.004 3
2	WX	44.9	20.40	0.004 1
2	PS	39.9	27.23	0.014 4
3	WX	52.0	38.29	0.006 6
3	PS	35.8	41.18	0.017 5
4	WX	185.4	77.37	0.036 7
4	PS	202.9	130.06	0.231 4
5	WX	317.3	160.72	0.077 0
5	PS	660.7	538.41	0.850 0
12	WX	3 306.9	2 705.39	8.368 4
12	PS	—	—	—
13	WX	5 790.5	2 382.08	19.519 8
13	PS	—	—	—

实验序号	算法	平均翻转次数	标准差	平均运行时间/s
1	WX	23.5	10.76	0.002 6
1	PS	16.3	11.69	0.004 3
2	WX	44.9	20.40	0.004 1
2	PS	39.9	27.23	0.014 4
3	WX	52.0	38.29	0.006 6
3	PS	35.8	41.18	0.017 5
4	WX	185.4	77.37	0.036 7
4	PS	202.9	130.06	0.231 4
5	WX	317.3	160.72	0.077 0
5	PS	660.7	538.41	0.850 0
12	WX	3 306.9	2 705.39	8.368 4
12	PS	—	—	—
13	WX	5 790.5	2 382.08	19.519 8
13	PS	—	—	—

实验序号	算法	平均翻转次数	标准差	平均运行时间/s
1	WX	64.2	36.14	0.005 8
1	PS	23.6	10.81	0.010 9
2	WX	296.4	208.62	0.027 9
2	PS	94.9	147.60	0.068 6
3	WX	199.9	103.09	0.025 1
3	PS	59.6	44.87	0.048 4
4	WX	721.9	378.92	0.194 9
4	PS	185.8	79.79	0.340 4
5	WX	4 569.2	3 430.71	1.546 0
5	PS	2 117.4	1 659.24	3.873 3

求解恰当可满足性问题的随机局部搜索算法

Stochastic local search algorithm for solving exact satisfiability problem

RichHTML

PDF

可视化

摘要/Abstract

引用本文

使用本文

图/表 5

参考文献 21

相关文章 3

编辑推荐

Metrics

[1]	武小年, 匡晶, 张润莲, 李灵琛. 基于SAT的GRANULE算法不可能差分分析[J]. 《计算机应用》唯一官方网站, 2024, 44(3): 797-804.
[2]	刘燕丽, 徐振兴, 熊丹. 基于动态奖惩的分支策略的SAT完备算法[J]. 计算机应用, 2017, 37(12): 3487-3492.
[3]	孙伟李艳灵鲁骏. 基于Partial MAX-SAT求解法的RBAC授权查询方法[J]. 计算机应用, 2013, 33(05): 1367-1390.