文章

文章链接 本文提出了一种基于**转移子句（Transition Clause）与递归模型旋转（Recursive Model Rotation, rmr）**的 MCS 枚举加速技术。

介绍文章前，首先需要说明对于经典的 SMT(QF_NIA)，基于 bit-blasting 做法，简而言之主要是以下三步：

Propositional Model Counting (MC) 即命题模型计数（\sharpSAT）是计算一个 CNF 公式 \mathcal{F} 中有多少个解（即 model）

这里简要解释：

文章链接 主要也只需要阅读 IPASIR 接口，一个 User-Friendly 的接口，通过重写这些接口来更好的调用 CaDiCaL 这个求解器

文章链接 这篇文章的前置版本可以查看 IPASIR 介绍，本文拓展了 IPASIR，加入了外部传播或者用户传播（UP）的拓展

文章链接

文章链接

文章链接 RoundingSAT 的工作可以看作者自己的网站：RoundingSAT，实验室名字也很有意思：MIAOresearch

文章链接 串行的算法中，引入了动态评分策略后，在并行的策略结合了种群的概念，引入了解池，通过共享高质量解与变量的极性密度（更倾向是 0/1）提高了跳出局部最优的能力

文章链接 在本工作中，我们重点关注提高 SLS 求解 PBO 的性能。

文章链接 与 代码链接 本文和 NuPBO CP'23 是同年的文章，因此没有对比，这篇文章的 实验效果 看了一下是不如 NuPBO 的效果 的，尤其是 300s 中 MWCB 和 SAP，NuPBO…

文章链接 提出了一种局部搜索求解 PBO 的框架，主要的思路就是把优化转为判定，由此可以使用 SAT 局部搜索求解器的思路，通过对约束加权（惩罚值），并由此进行打分函数的设计，从而指导启发式算法工作…

文章链接 本文提出了一种针对 局部 基数约束的局部搜索算法 LS-ECNF ，通过 ECNF 的形式，可以避免将基数约束编码为 SAT，从而获取更好的求解性能 本文的后续改进为 LS-PBO SAT'…

文章链接 在 SAT 问题的全局约束中，如果将约束编码为 SAT，会导致变量与子句的急速膨胀，造成求解困难。但有时候，编码的辅助变量又属于 nogood 类型的变量，能够指导搜索的过程。

文章链接 对于一个哈密顿量，我们总可以把它拆成若干部分之和： 又根据含时哈密顿量在薛定谔方程中的解，我们可以得出 U(H, t) = \exp{(\frac{-iHt}{\hbar})} 根据 Tro…

文章链接 主要的贡献为：

文章链接