#CCF

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

动机 前言 介绍文章前，首先需要说明对于经典的 SMT(QF_NIA)，基于 bit-blasting 做法，简而言之主要是以下三步： 先给整数变量一个有限位宽（bit-width）把整数运算翻译成位向量电路再交给 SAT solver 对于第一步而言，一个整数变量 x 其位向量可以表示为位宽为 w 的向量 \bar{x}: <\bar{x}_{w-1}, \cdots, \bar{x}_1, \bar{x}_0>，其中 \bar{x}_{w-1} 为符号位 。

[!tip]一篇综述，请教师兄关于 MC 内容的时候师兄给的，主要说的是偏应用的 MC为了面试的时候对 MC 有个大概的了解，临时抱的佛脚 问题介绍 Propositional Model Counting (MC) 即命题模型计数（\sharpSAT）是计算一个 CNF 公式 \mathcal{F} 中有多少个解（即 model） [!note] 与 AllSAT 的区别AllSAT 要求 枚举 (Enumerate) 所有满足公式的变量赋值MC 只要求找到有多少组满足公式

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.

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

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

[!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]文章链接串行的算法中，引入了动态评分策略后，在并行的策略结合了种群的概念，引入了解池，通过共享高质量解与变量的极性密度（更倾向是 0/1）提高了跳出局部最优的能力 ParLS-PBO: A Parallel Local Search Solver for Pseudo Boolean Optimization [!abstract]-As a broadly applied technique in numerous optimization problems,

[!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

[!tldr]文章链接通过绝热定理，我们可以写出哈密顿量的一个形式：H = \sum_{i = 1}^NH_i又根据含时哈密顿量在薛定谔方程中的解，我们可以得出 U(H, t) = \exp{(\frac{-iHt}{\hbar})}根据 Trotter-Suzuki decomposition e^{A +B} \simeq (e^{\frac{A}{n}}e^{\frac{B}{n}})^n我们可以将系统最终演化酉变换写为：U(H, t, p) = \prod^p_{j=

[!tldr]文章链接 与 代码链接本文和 是同年的文章，因此没有对比，这篇文章的 看了一下是不如 的，尤其是 300s 中 MWCB 和 SAP，NuPBO 能够全部都比 好，但本文有一些还是不如 LS-PBO，甚至在 中直接注明了 DeciLS-PBO 被 NuPBO 和 DLS-PBO 支配了 DeciLS-PBO: an Effective Local Search Method for Pseudo-Boolean Optimization [!abstract]-

[!tldr]文章链接提出了一种局部搜索求解 PBO 的框架，主要的思路就是把优化转为判定，由此可以使用 SAT 局部搜索求解器的思路，通过对约束加权（惩罚值），并由此进行打分函数的设计，从而指导启发式算法工作本文后续的改进版有：， ， Efficient Local Search for Pseudo Boolean Optimization [!abstract]-Pseudo-Boolean Optimization (PBO) can be used to model

[!tldr]文章链接本文提出了一种针对 局部 基数约束的局部搜索算法 LS-ECNF ，通过 ECNF 的形式，可以避免将基数约束编码为 SAT，从而获取更好的求解性能本文的后续改进为 ，值得注意的是，本文提出的 基数约束 本质上是一种特殊 形式 Extended Conjunctive Normal Form and An Efficient Algorithm for Cardinality Constraints [!abstract]Satisfiability (S

[!tldr]文章链接 TLSF: a new dynamic memory allocator for real-time systems [!abstract]-Dynamic storage allocation (DSA) algorithms play an important role in the modern software engineering paradigms and techniques (such as object oriented progr

[!tldr]文章链接主要的贡献为：将 PBO 问题编码为 QAOA 的形式将 QAOA 分割为子问题进行分布式求解 Local to Global: A Distributed Quantum Approximate Optimization Algorithm for Pseudo-Boolean Optimization Problems [!abstract]-With the rapid advancement of quantum computing, Quant