李 壮,刘 磊,张桐搏,周文博,吕 帅

1(吉林大学 计算机科学与技术学院,吉林 长春 1 30012)

2(符号计算与知识工程教育部重点实验室(吉林大学),吉林 长春 130012)

可满足性问题(SAT)是公认的第一个NP-完全问题,是人工智能领域最重要的研究方向之一.自人工智能发展初期就引起了研究者的广泛关注,当今SAT 求解器已能够解决很多现实问题.近年来,国内外的学者致力于求解SAT问题的效率和求解能力,提出了多种方法.

1992年,Selman 等人提出的GSAT 算法证明了局部搜索算法可以应用于求解SAT 问题,其强大的求解能力为局部搜索求解SAT 问题奠定了基础[1].随着局部搜索方法在该领域的广泛应用,自2002年SAT 比赛的开展以来,众多基于局部搜索算法的求解器也相继问世并展现出了各自强大的求解能力.2005年,Li 等人提出了g2wsat类算法,该算法结合随机选择和贪心双模式,在求解的过程中展现出良好的性能[2].2011年,Li 等人提出了利用变量可满足历史记录的局部搜索求解器SatTime,获得SAT 2011 随机组银奖[3].2016年,KhudaBukhsh 等人提出了SATenstein 求解框架,该框架结合了多个高性能局部搜索求解器,其求解效果胜过多个主流求解器[4].近年来,由Cai 等人提出的基于局部搜索的格局检测策略成为SAT 比赛中最具影响力的策略之一.2011年,Cai 等人设计的SWCC 算法及相关求解器皆使SAT 求解器的计算能力得到巨大地提升,并取得惊人的成绩[5].随后,Cai 等人于2012年提出的CCASat 获得SAT 20 12年随机组金奖[6].2014年,Cai 等人提出的CSCCSat 获得SAT 201 4年比赛Hard-combinatorial 组铜奖和SAT 2016 比赛Random track 组银奖[7].同时,基于局部搜索的格……