Journal of Computer Applications ›› 2024, Vol. 44 ›› Issue (3): 842-848.DOI: 10.11772/j.issn.1001-9081.2023030364

• Advanced computing • Previous Articles     Next Articles

Stochastic local search algorithm for solving exact satisfiability problem

Xingyu ZHAO1, Xiaofeng WANG1,2(), Yi YANG1, Lichao PANG1, Lan YANG1   

  1. 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)


赵星宇1, 王晓峰1,2(), 杨易1, 庞立超1, 杨澜1   

  1. 1.北方民族大学 计算机科学与工程学院,银川 750021
    2.图像图形智能处理国家民委重点实验室(北方民族大学),银川 750021
  • 通讯作者: 王晓峰
  • 作者简介:赵星宇(1999—),男,湖北荆州人,硕士研究生,CCF会员,主要研究方向:算法分析与设计
  • 基金资助:


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



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

CLC Number: