#主题/SAT

[!attention] 免责声明此文章由 Claude Code 阅读生成，本人仅作为搬运，有错误的地方与本人无关（ [!tldr]文章链接本文提出了一种基于**转移子句（Transition Clause）与递归模型旋转（Recursive Model Rotation, rmr）**的 MCS 枚举加速技术。

[!important]这份调研阅读了很多份论文，这里会使用一个 biblatex 来给出引用，调研有一份 Typst 版，可以参考 NAE-SAT Definition 首先，我们重申 SAT 的定义： Definition 1：对于一个给定的 CNF 公式 c_1 \wedge \dots \wedge c_m，其中 c_i = \bigvee^t_j x_t 且 t \geq 1, t \in \mathbb{Z}，是否存在一组赋值 \phi = (x_1, \dots

现有的 SAT 并行求解策略主要分为两类：分治法以及基于组合策略的并行。

Problem Partitioning via Proof Prefixes [!tip]前置知识：Cube & ConquerClause Proof 这里简要解释： Cube & Conquer 是一种并行方法，本质上是对解空间的一次静态划分，选择一个良好的变量序列作为假设（cube），将解空间划分为多个不相交的子集，然后每个解空间都通过一个线程独立求解子句证明（以 LRAT 为例）：本质上是 CNF 的证明序列，用于说明 UNSAT 为什么 UNSAT，通过不断对这个

[!tldr]文章链接 From Clauses to Klauses [!abstract]Satisfiability (SAT) solvers have been using the same input format for decades: a formula in conjunctive normal form.

这里放一些我学习 SAT 求解器的文章，应该会是卡片式的，阅读的书籍为： TAOCP 4BHandbook of SatisfiabilityHandbook of Parallel Constraint Reasoning 以及各种论文还有比较有代表性的的 CDCL 求解器 在 SAT 问题中有需要专业名词（膨胀出来的），对于这些专业名词，我们会在文章中进行解释，不做统一的名词表 SAT 问题基本定义 精确算法 分支启发式策略 其他拓展

[!tldr]文章链接这篇文章的前置版本可以查看 ，本文拓展了 IPASIR，加入了外部传播或者用户传播（UP）的拓展 Overview 我们所提出的扩展允许用户： 在搜索过程中检查 trail 的变更并接收相关通知在求解过程中无需重启搜索即可向问题中添加子句基于外部知识直接传播文字，而无需显式添加原因子句（即采用延迟的按需解释机制）。

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

复习一些数学知识 [!note]在最开始，我们复习一些基础的离散数学，主要是一元逻辑部分，我们默认读者有基本的位运算基础，如果没有的话，可以查看下面进行学习[!hint] 位运算 位运算主要为与，或，非三种，表示为 \&, |, \neg，其中，前面两种为二元运算，非运算为一元运算，其真值表的变化为：y&x01000101y|x01001111\negx0110 我们首先引入一个记号 \mathbb{B} = \{0, 1\}，这是一元逻辑中所有变量的定义域 我们称 \for

前言 在 中，我们引入了命题逻辑（Propositional Logic）来编码与表达现实问题，但我们知道，Propositional Logic 的表达能力本质上并不是很强，对于一些复杂的问题，我们需要拐着弯通过各种 encoding trick/tweak 用纯粹的命题逻辑 "强行" 表达/抽象 arithmetic 有关的问题。

相位 [!info] 相位（Phase）在 SAT 求解器中，相位通常指变量在搜索过程中的初始赋值偏好或历史状态或者简单来说： 我们需要对变量的决策赋值，这个赋值的选择我们叫作相位（赋值为真/假） CaDiCaL 中如何选择相位进行赋值 值得注意的是，相位的选择本质上就是二叉树先搜索哪一边，因此在理论上相位的选择对求解速度应该没有那么大的影响，赋真/假都是只有 50% 的概率猜对。

前言 在 SAT 的精确算法中，其框架都是基于分支限界算法，其主体框架如下： while True: conf = propagation() if conf is None: decide() else: resolve() 其中，resolve 用于回溯以撤销冲突的赋值，decide 用于决策变量的赋值，并继续探索树的下一层级，所有被决策的变量都会被记录到 trail 中，用于冲突时撤销赋值 如果我们想要求解的更快，那么决策的变量顺序是十分重要的 [!tip]在树搜索中，

[!tldr]文章链接主要也只需要阅读 IPASIR 接口，一个 User-Friendly 的接口，通过重写这些接口来更好的调用 CaDiCaL 这个求解器 API Overview [!note] 求解器的状态我们假定求解器会返回以下几种状态：UNKNOWNSOLVINGSATUNSAT 主要给出了九个函数接口： const char *ipasir_signature (void); void *ipasir_init (void); void ipasir_relea

[!tldr]文章链接 The Impact of Literal Sorting on Cardinality Constraint Encodings [!summary]The effectiveness of satisfiability solvers strongly depends on the quality of the encoding of a given problem into conjunctive normal form.

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

[!tldr]文章链接在 SAT 问题的全局约束中，如果将约束编码为 SAT，会导致变量与子句的急速膨胀，造成求解困难。

[!tldr]文章链接RoundingSAT 的工作可以看作者自己的网站：RoundingSAT，实验室名字也很有意思：MIAOresearch Divide and Conquer: Towards Faster Pseudo-Boolean Solving [!abstract]The last 20 years have seen dramatic improvements in the performance of algorithms for Boolean sat