转自微博用户：蔡少伟 （中科院软件所研究院，智源青年科学家）

记一下最近我们发表的两篇论文。我觉得这两篇是SAT(布尔约束求解)和SMT(谓词逻辑上的约束求解)方向值得被了解的事情，也对应了我们这几年的工作。

一篇做SMT求解器, 发在CAV 2022会议(形式化验证顶级会议)；
一篇做SAT求解器，发在Journal of Artificial Intelligence Research (和AIJ并称 AI两大综合性期刊，传统AI方向主要期刊之一)。

1. Shaowei Cai, Bohan Li, Xindi Zhang, "Local Search For SMT on Linear Integer Arithmetic", CAV 2022.

我们团队自研的线性整数算术SMT求解器LS-LIA。 这是首个支撑整数理论的随机搜索求解器，区别于主流的DPLL(T)方法。
我们的求解器在标准测试集SMTLIB上已经和前沿求解器包括Z3，CVC5, YICS2, MathSAT5等达到竞争性和互补性的效果。结合LS-LIA和Z3的混合求解器可以在SMTLIB的测试集上做到目前最好效果。实际上，我们去年的一个基于此方法的SMT求解器就拿到了SMT Competition差分逻辑组的冠军，国内首次SMT比赛夺冠。

正如Metareview里提到的，希望这篇论文为SMT求解带来新的思路并有更多follow-up工作。”The paper introduces a first local search algorithm for LIA, which works well on various families. Local search is already an important component in modern decision procedures (e.g., SAT, BV) and the reviewers are hopeful that the paper will lead to follow-up works.“

2. Shaowei Cai, Xindi Zhang, Mathias Fluery, Armin Biere, "Better Decision Heuristics in CDCL through Local Search and Target Phases", Journal of Artificial Intelligence Research (accepted). Best Paper受邀论文。

这篇论文的背景是，我们提出的CDCL求解+局部搜索采样的混合求解方法发表在去年SAT会议上，拿了Best Paper Award （从2017年就开始做了，在2021年终于发表），因此JAIR期刊邀稿我们扩展此工作投过去，很快可以接受。本来是受邀扩展的论文，很快完成就可以。但我觉得这不是一篇论文的事情，而是考虑如何把SAT混合求解研究的现状讲清楚，因此和SAT求解的另一个主要团队Armin Biere (SAT协会主席)讨论了此事，花了大约一年的时间一起合作了一篇长文 （在2021 SAT线上会议我们讨论彼此的技术路线的时候，越说越起劲，然后决定我们合作介绍这个方向的前沿技术，也介绍我们两个作为此方向的主要团队，各自的发展路线）。这篇 可以说是近些年混合SAT求解器的集大成的工作。

文章不但介绍了我们两个团队各自的工作，最后也把二者的技术做了些融合，并做了非常大量的实验评估和分析。此外，本文除了技术贡献，比较有趣的地方还在于对目前主要的混合求解技术提供了清晰的viewpoint，讲了一个”双城记“。如一个审稿人说”I have found the article a pleasure to read overall. The authors succeeded in writing a coherent story and gave both ample background (which I particularly enjoyed) and lots of interesting details to make the article worth a read.“
 

内容中包含的图片若涉及版权问题，请及时与我们联系删除