#研究/SAT

现有的 SAT 并行求解策略主要分为两类：分治法以及基于组合策略的并行。二者通常都会进一步与子句共享（Clause Sharing）结合。

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

首先，我们重申 SAT 的定义：

这里简要解释：

文章链接

这里放一些我学习 SAT 求解器的文章，应该会是卡片式的，阅读的书籍为：

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

当 BCP 完成后，如果在这个过程中发现了冲突（有一个子句的文字全部为假），那么我们认为发生了冲突，需要撤销赋值并回溯。

我们首先引入一个记号 \mathbb{B} = \{0, 1\}，这是一元逻辑中所有变量的定义域

在 SAT 中，我们引入了命题逻辑（Propositional Logic）来编码与表达现实问题，但我们知道，Propositional Logic 的表达能力本质上并不是很强，对于一些复杂的问题，我…

值得注意的是，相位的选择本质上就是二叉树先搜索哪一边，因此在理论上相位的选择对求解速度应该没有那么大的影响，赋真/假都是只有 50% 的概率猜对。

每个变量的 score 为其在所有子句中的文字出现次数。

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

文章链接

从布尔约束传播出发，介绍观察字和双观察字的维护与传播流程。

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

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