#研究

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

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

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

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

一个一开始完全不知道怎么做的实验

-文再文 介绍的两份 LLM + OR 工作：

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

这里简要解释：

文章链接

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

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

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

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

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

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

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

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

MCP(Model Context Protocol) 是 Anthropic 在 2024 年 11 月推出的开源协议，用于将 AI 连接到外部的应用程序上，本质上是一个标准，规定了应用程序应该如何…

SparseTIR 与 SparTA 的实验复现

由于在 Windows 下开WSL和IDE导致电脑内存已经吃不消了，所以我直接把电脑系统刷成了 Linux （彻底疯狂了），这里记录一下我的配置过程

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

文章链接

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

量子本质上可以通过量子化进行得到，当我们对一个宏观物体进行无限细分后，直到不得不靠“几个原子”这种单位去描述物体的长度时，量子效应就出场了。

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

世界上大名鼎鼎的系统实验室 PDOS 开设的课程，教授这门课的教授包括：

只针对 Windows 系统

Lab1 的内容是简单的熟悉 xv6 操作系统和怎么做实验，官网上对实验难度的描述是easy , easy, moderate/hard, moderate, moderate。

Lab2 熟悉一些系统调用，这个实验有一些小坑 😤

你说的 easy 不是 easy，我说的 hard 是什么 hard😭，实验难度 easy, easy, hard，结果第一题差点把我送走了……MIT，你坏事做尽 😭

2020 年的课和这个不太兼容（需要看完中断之后才能做这个实验），实验难度为 easy, moderate, hard。

实验早就做好了但是…… 思路借鉴了课程中 Prof. Robert Morris 的思路，实验只有一题但是是 hard

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

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

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

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

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

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

文章链接

文章链接 主要的贡献为：

这里记录了我在 ICT 的实习历程，实习的时间为 2023-06-01 到 2023-07-10

一个传统的线性回归讲义

内存管理，伙伴系统（Buddy System）与页表配置（Page Table） 重回中文写作

熟悉现代 C++17 的一个小型实验，由于条约限制，所以在这里不会把代码放出来Primer

Stanford CS143 实验环境安装与配置

Assignment 1 实现词法分析器

CS144 的一些准备工作

实现一个 best effort 的字节传输流

实现重组字节流

写出完整的 TCP Receiver

Stanford CS144 Spring 2023 实验环境与 Lab0

很有意思的实验，至少在我做过的里面这个带来的正反馈是最多的

这个实验倒是比较简单，没什么可说的

一个做了很久，做完之后其实还挺有收获的实验（我愿称之为最难🥺）

一些搭建环境的远古方法

不如我自己写的 `shell` 难度大（不过关于信号处理的部分还是很有意思的）

实现 chrt 系统调用（简易版）

HttpServer

为什么MINIX你是微内核！我不理解！

实现一个简易版的Shell，可以识别一些简单到不能再简单的命令（bushi

MINIX3 内存管理

一个模拟多线程的实验，应该算是比较简单的实验，可以仿照原有的实现来做。

使用 E1000 网卡写一个驱动程序

优化 xv6 中的锁结构

实现 MapReduce 框架，虽然都说很简单，但是比较菜的我还是写了好几天，因为一开始不会Go，所以不知道从何下手

ICS PA 的实验环境准备

ICS PA1 sdb

实现一个 pstree 的 shell 小工具（实际是 pstree 的一个阉割版本）

Project Setup & Simple Test

SparseTIR 解读（论文、源码 ）

介绍如何在一台只有 docker 的环境的服务器下配置 tvm 运行环境

梳理 PBO 局部搜索求解器的打分函数、约束加权策略及算法之间的继承关系。

编译原理的一些简单复习

这部分是一个拓展，文中的图片来源于李宏毅老师的ppt

感知机(perceptron) 是一种二分类的线性分类模型，也就是说，输入数据通过模型运算后可以输出分类的类别，由于是二分类，所以类比只有 +1, -1

NJU 十分知名的课程，不过在 21 年之前似乎还没有如今的名气。

国内第一操作系统实验室 IPADS 的作品， IPADS 的所长陈海波老师（Prof.

作为 CMU 数据库的入门课，这门课由数据库领域的大牛 Andy Pavlo 讲授（“这个世界上我只在乎两件事，一是我的老婆，二就是数据库”）。

斯坦福的编译原理课程，设计者开发了一个 Classroom-Object-Oriented-Language，简称 COOL 语言。

这门课的主讲人之一是网络领域的巨擘 Nick McKeown 教授。这位拥有自己创业公司的学界业界双巨佬会在他慕课每一章节的最后采访一位业界的高管或者学界的高人，非常开阔眼界。

CMU 大名鼎鼎的镇系神课，以其内容庞杂，Project 巨难而闻名遐迩。

这门课和 MIT 6.S081 一样，出品自 MIT 大名鼎鼎的 PDOS 实验室，授课老师 Robert Morris 教授曾是一位顶尖黑客，世界上第一个蠕虫病毒 Morris 病毒就是出自他之手。

由 Zihao Yu 设计实现的大名鼎鼎的 NJU PA，课程资料详细，难度较大，但仔细阅读材料后，总能自己解决问题，课程的正反馈很强，一门很好的系统入门课（包括编程习惯上也是很好的入门课）

这门课让我记忆犹新的有两个部分：

明确论文发表的时间为 2022 年，在这个时间段，算力的提升使得 DNN 的层数能够越来越深，模型越来越复杂。此时，为了提高 DNN 效率而必须进行稀疏化，也就是尽可能地减少不必要的数据冗余。

关于 PyTorch2.0 中对 Dynamo 的解析