基数约束 SAT 并行策略Problem Partitioning via Proof Prefixes [!tip]前置知识：Cube & ConquerClause Proof 这里简要解释： Cube & Conquer 是一种并行方法，本质上是对解空间的一次静态划分，选择一个良好的变量序列作为假设（cube），将解空间划分为多个不相交的子集，然后每个解空间都通过一个线程独立求解子句证明（以 LRAT 为例）：本质上是 CNF 的证明序列，用于说明 UNSAT 为什么 UNSAT，通过不断对这个
IPASIR-UP: User Propagators for CDCL[!tldr]文章链接这篇文章的前置版本可以查看 ，本文拓展了 IPASIR，加入了外部传播或者用户传播（UP）的拓展 Overview 我们所提出的扩展允许用户： 在搜索过程中检查 trail 的变更并接收相关通知在求解过程中无需重启搜索即可向问题中添加子句基于外部知识直接传播文字，而无需显式添加原因子句（即采用延迟的按需解释机制）。
LS-PBO 阅读笔记[!tldr]文章链接提出了一种局部搜索求解 PBO 的框架，主要的思路就是把优化转为判定，由此可以使用 SAT 局部搜索求解器的思路，通过对约束加权（惩罚值），并由此进行打分函数的设计，从而指导启发式算法工作本文后续的改进版有：， ， Efficient Local Search for Pseudo Boolean Optimization [!abstract]-Pseudo-Boolean Optimization (PBO) can be used to model