栞忘れてください
A DIGITAL GARDEN

文章

144 则笔记，53 个主题，慢慢生长。

01

公开课实验

SJTU 操作系统简介

SJTU 操作系统简介

课程简介 所属大学SJTU先修课程要求良好英语水平 + 计算机系统 + 少量体系结构编程语言要求C + ARM(aarch64) 汇编课程网站SJTU SE315 Course Website 国内第一操作系统实验室 IPADS 的作品， IPADS 的所长陈海波老师（Prof.

Machine Boot

Set the envrionment and boot the machine

内存管理

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

CMU Database

CMU Database

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

Project#0

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

CS143 编译原理

CS143 编译原理

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

Lab1 词法分析

Assignment 1 实现词法分析器

CS144 计算机网络

CS144 计算机网络

课程简介 这门课的主讲人之一是网络领域的巨擘 Nick McKeown 教授。

Lab2 TCP Receiver

写出完整的 TCP Receiver

Lab1 重组字节流

实现重组字节流

Lab0 字节传输流

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

CMU CSAPP

CMU CSAPP

[!cite]从 csdiy 的简介中复制过来，并不是本人所写，下文中所有的 “本人” 均指代 Yinmin Zhong 课程简介 CMU 大名鼎鼎的镇系神课，以其内容庞杂，Project 巨难而闻名遐迩。

cache-lab

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

shell-lab

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

attack-lab

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

bomb-lab

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

data-lab

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

ECNU 数据学院相关

2020 OS_HW3 RAM与Disk读写速度对比

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

2020 OS_HW2 chrt

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

2020 OS_HW1 shell

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

MIT 6.S081操作系统

MIT 6.S081操作系统

课程简介 所属大学MIT先修课程要求良好英语水平 + 计算机系统 + 少量体系结构编程语言要求C + 少量 RISC-V 汇编课程网站MIT 6.S081 Course Website 世界上大名鼎鼎的系统实验室 PDOS 开设的课程，教授这门课的教授包括： Robert MorrisFrans Kaashoek 两名教授在操作系统方向造诣深厚，Prof.

Lab7 Networking

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

Lab6 Multithreading

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

Lab5 CoW Fork

实验早就做好了但是…… 思路借鉴了课程中 Prof.

Lab4 Trap

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

Lab3 Page Tables

你说的 easy 不是 easy，我说的 hard 是什么 hard😭，实验难度 easy, easy, hard，结果第一题差点把我送走了……MIT，你坏事做尽 😭 实验准备 把第三章看懂（条件很简单，也很 tm 难，第三章应该是我目前为止没有把英文原本读完的一章了，实在是看不下去啊 😭），可以读中文版，也可以阅读*《现代操作系统：原理与实现》*（处理器架构有所不同但无伤大雅）。

Lab0 Tools

实验准备 只针对 Windows 系统 首先，需要安装 WSL2（Windows Subsystem for Linux 2），使用 Ubuntu，具体的教程可见微软官网打开 Ubuntu 命令行，运行如下两条命令： sudo apt-get update && sudo apt-get upgrade sudo apt-get install git build-essential gdb-multiarch qemu-system-misc gcc-riscv64-lin

Lab1 Utils

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

Lab2 System Call

Lab2 熟悉一些系统调用，这个实验有一些小坑 😤 实验准备 运行Lab: System calls (mit.edu)上的命令 git fetch git checkout syscall make clean 即可得到该实验的实验环境了。

MIT 6.824 分布式系统

MIT 6.824 分布式系统

[!cite]从 csdiy 的简介中复制过来，并不是本人所写，下文中所有的 “本人” 均指代 Yinmin Zhong 课程简介 这门课和 一样，出品自 MIT 大名鼎鼎的 PDOS 实验室，授课老师 Robert Morris 教授曾是一位顶尖黑客，世界上第一个蠕虫病毒 Morris 病毒就是出自他之手。

Lab1 MapReduce

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

NJU 计算机系统导论

NJU 计算机系统导论

课程简介 [!cite]理解"程序如何在计算机上运行"的根本途径是从"零"开始实现一个完整的计算机系统.

NJU 操作系统简介

NJU 操作系统简介

课程简介 所属大学NJU先修课程要求良好英语水平 + NJU ICS编程语言要求C课程网站蒋炎岩老师的主页 NJU 十分知名的课程，不过在 21 年之前似乎还没有如今的名气。

M1 打印进程树 (pstree) 实验指北

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

PKU & UCB 操作系统

PKU & UCB 操作系统

[!cite]从 UCB CS162 的简介中复制过来，并不是本人所写，下文中所有的 “本人” 均指代 Yinmin Zhong 课程简介 所属大学：UC Berkeley先修要求：CS61A, CS61B, CS61C编程语言：C, x86 汇编课程难度：🌟🌟🌟🌟🌟🌟预计学时：200 小时+，上不封顶 这门课让我记忆犹新的有两个部分： 首先是教材，这本书用的教材 Operating Systems: Principles and Practice (2nd Ed

02

差生文具店

从 Quartz 到 Astro

记录一次博客搬家：为什么离开 Quartz，怎样用 Astro 保留 Obsidian 的双链体验，以及重新掌握博客编译过程的取舍

通过 submodule 发布博客

前情提要 由于在 Obsidian 中，虽然我有不被 git 追踪的文件夹（私有文件夹），但是这也限制了我 的需求（因为 Windows 上的 iCloud 十分难用） 因此，我们期望工作流程如下： 在私有仓库中更新博客在公开仓库中拉取博客内容并自动构建 本质上，我们将公开仓库作为了一个博客生成器，专门用来触发 CI GitHub 与本地设置 GitHub 首先，需要申请一个 个人 Token，名字自由命名，例如 BLOGS，但是记得复制这个 Token，例如 <TOKEN>

科研绘图工具

配色 可以在平时阅读时保存一些好看图像的配色/架构，例如 或者可以直接参考 配色网站，不过比较麻烦的是得自己去找颜色 绘图 AI 辅助 用提示词生成绘图脚本，例如仙人掌图（cactus）的代码如下： import pandas as pd import matplotlib.pyplot as plt import os import numpy as np # --- 配置参数 --- # CSV文件所在的目录 # EXPR_NAME = "MagicSquare-LS"

创作时间

使用实验配置文件来生成脚本

[!info] 前言这是我最近才开始实验的工作流，目前还比较粗糙，后续应该会慢慢改进 情景 假设现在我在 benchmark 中有多组例子，benchmark/B1，benchmark/B2，benchmark/B3 在 bin 中有多个求解器（不一定是 bin，规定好路径即可），bin/A， bin/B，bin/C 现在，我想跑所有求解器在 benchmark/B1 上的结果 如果按照 的做法，我们会需要自己写 n 个脚本（与求解器数量一致），每个求解器面临参数设置不同，输

记录一次 Ubuntu 扩盘

起因 由于组内服务器先前 CPU 坏了（难以见到的事情但是被我们遇上了），导致重装了两次系统： 第一次装在了 /dev/sdb 这个机械硬盘内（6.5T）且开了 LVM 第二次装在了 /dev/sda 这个 SSD 里（900G），但没有开 LVM 在第二次装的时候，没有把 /dev/sdb 这个机械硬盘加入到系统内，导致整个系统可用磁盘空间只有不到 900 G 运行 lsblk 如下图所示： 而现在这个 SSD 的空间完全不够用了，因此需要把原本没挂载的机械硬盘挂上，并启用

GTest 单元测试模板

[!warning]本文不是教程，只是一个模板，方便本人复制粘贴而已部分内容参考自博客 GTest / GMock 单元测试实践手册，详细的可以进博客学习 项目架构 假定项目的结构为： . ├── build ├── CMakeLists.txt ├── Makefile ├── README.md ├── scripts ├── src │ └── main.cpp └── tests ├── CMakeLists.txt └── tree.cpp 我们在 tests 中写

实验结束自动发送邮件

[!attention] 免责声明脚本几乎都是 AI 实现的，请注意甄别 [!info] Enhancement一个想法是通过建立一个服务，用于监听进程名称，如果限制的进程名称已经跑完了，那就发送邮件，感觉可以考虑写一个跑在后台的 flask（前后端+SQLite），增删改查一下，感觉还是很有戏的 前言 在跑实验的时候经常会遇到以下情况 按照 中提到的，我们会通过 cat run.sh | xargs 来并行实验，然而每个例子跑的时间是不确定的，有时候设置时限为 3600 s

Quartz 使用 Bun 替换 Nodejs

[!info] 写在前面只是心血来潮，想要更换一下 Quartz 的包管理器以及打包工具，之前一直听说 Bun 运行时的速度快，想着在本地预览的话应该会比 Node 更快，所以替换一下 本地更改 首先需要安装一下 bun ，我是用的是 MacOS （根据官网给出的命令安装即可） 然后，我们需要更改 quartz 的几个文件： package.json 这里主要是更改 scripts 中的内容： "scripts": { "quartz": "./quartz/bootstra

MacOS 软件推荐

[!tip] 前言我个人选择的基本都是一些开源软件（有些不开源但是好用的也没办法）还可以参考网站 Awesome Mac，探索更多软件 包管理器 由于 MacOS 本质上还是个 Unix-like 的系统，因此还是离不开包管理器，用起来也更加方便，我使用的是 HomeBrew ，应该算比较大众的选择。

MacOS 配置 RIME + 雾凇

[!tip] 前言由于 MacOS 自带的输入法没找到怎么 shift 切换输入法，本身切换输入法的按键被我改成 control 了，而且之前在 下一直在用小企鹅+雾凇，对雾凇这个词库很有好感（，所以在这里替换一下 [!bug] 已知 BUG在 MacOS 下已知的 bug 有两个：在Mac上按cmd+tab切换应用后，输入法会自动打出‘a’github issue栏中打字会出现多余字符 RIME 首先我们通过 brew 来安装鼠须管： brew install squirr

间接解决 Docker 中发送邮件后无法收到

问题记录 [!attention] 前置知识注意，这里我们使用的是 Gin 这个 web 框架开发的后端，我们使用了 gomail.v2 来发送文件，template 来渲染我们的 html 文件（也就是要发送的邮件内容），函数如下所示 // In package model type MailInfo struct { Subject string Code string ToWho string } func sendEmailVerificationCode(data

docker compose 部署 web 项目

前期提要 [!note] 动机由于一直以来部署项目都十分麻烦，一下子有测试服务器一下子有正式服务器，正式生产环境的服务器还没办法使用 ip 访问，域名合法前也没办法访问网站。

阿里云新建用户无法 SSH

起因 购买了一个阿里云的服务器，选择的是通过 Ubuntu-24.04 镜像生成的 买完之后没给我密码，只有这样一个界面 没有账号和密码，只能通过这里的远程连接，用浏览器暂时配置一下 打开后，我们进入 admin 这个账户，其 sudo 不需要输入密码，可以直接 sudo su 切换到 root 第一步，我们先创建账号： sudo su adduser virgil adduser virgil sudo 其中，第二步我们还需要输入密码和一些配置，配置可以一直回车，让其保持缺

strcpy 中的 overlap 问题

起因 我们有以下代码： void remove_leading_zeros(char *str) { int i = 0; while (str[i] == '0' && str[i + 1] != '\0') { i++; } if (i > 0) { strcpy(str, str + i); } } 在运行这个函数时，假设我们的代码如下： char* s = "0077160493132716049313271604931327160493"; remove_leadi

如何在 Windows 上使用 Linux

[!tip]考虑到代码基本都在服务器上跑，为了兼容性，在本地开发的时候最好也使用 Linux 或 MacOS环境进行开发 一些文档帮助 关于 WSL 的下载，安装和使用，在微软的 官方文档 中有详细的介绍。

学术 Slides 的制作

关于 Slides 的制作，有三种方式： 传统的 PPTBeamer 风格的学术 SlidesReval.js 网页 Slides 三种方式可以自由选择，优缺点如下： PPT 的制作稍微简单，不需要做任何动画，也不需要花里胡哨的模板（很适合赶工的时候做），但缺陷很明显，数学和代码的支持很差，有时候只能截个图放上去，很不美观（不美观的数学公式会让人难以理解……也生不出看下去的欲望）Beamer 模板写起来困难，但数学公式和代码都较为美观，并且模板问题难以解决，毕竟不是每个人都有

创作时间

代码编辑器推荐

本地环境 使用的设备均为 Windows11 系统： 本地台式：14700KF + 4080S + 32G + 2TB本地笔记本：13th-i5 + 16G + 1TB 一般而言都是在台式机上干重活（相当于会跑一下代码测试一下），笔记本对我来说是一个 ssh 工具，或者是简单写一个不吃配置的代码的工具 开发环境使用的是 WSL2-Ubuntu-24.04 + Windows，其中： WSL2 主要用来写科研代码，因为经常用到 C++/C， Rust， Python 和 Bas

VSCode 的赛博暖暖

这里主要是一些赛博暖暖的内容，不涉及任何功能上的配置 主题 Github Theme Dark Default，高亮如下所示： [!tip]之前使用的主题是 Tokyo Night，也很好看，换这个是因为在我之前的笔记本上，感觉完全的黑色+透明度更适合那个 Archlinux 的桌面背景（ 图标主题 Material Icon Theme，这里主要是用来更好的显示文件夹的图标，看起来花哨一些（ 字体 中文 霞鹜文楷，代码 Monaco，配置的方法如下：打开设置后（Ctrl +

在 VSCode 中使用 AI

在这里推荐一些 AI 插件，用于增强 VSCode 的代码体验 [!attention] Out-of-Date由于本人已经很久没有用 VSC 了，插件的认知停留在 2025-01 左右的时间 Github Copilot 如果你已经申请了 Github 的黄书包（也就是教育版本），那么你可以免费使用 Copilot ，这是一个 LLM 代码补全工具，补全程度甚至可以自己写代码，有了这个，程序员只需要当无情的 Tab 键入机器就行。

OrbStack 占用过多磁盘空间

创作时间

[!attention] 免责声明本文的内容非原创，只是转载与记录，防止自己老是忘记命令还得去查 前期提要 这篇文章主要记录使用 OrbStack 后， 时导致的磁盘空间消耗过多的解决方法 [!hint]说是解决方法，其实只是一次搬运而已 这个问题在 Github 上有人提到，并且在评论的最下方给了一个暂时的解决方法 解决方法 容器、镜像与卷的清理，都可以通过 OrbStack 的图形化界面来进行删除，但构建时的缓存只能通过命令来删除： docker builder prun

Obsidian 插件推荐

创作时间

[!info] 前言插件来来去去，更换了很多，最终留下来的比较趁手的其实也就几个，这里一一介绍 目前的外观如下： 外观美化 主题 主题本人用过的有（按照时间顺序给出） Blue TopazBorderPrimaryVelocity 目前正在使用的是 Velocity，原因是与 Mac 非常适配，前面的主题如果自己花心思配置的话，也是很好看的（和个人审美有关系，这不是本文的重点） [!important] 重要提示上述主题都需要通过下文中的 插件中的 Style Setting

Obsidian 多设备同步

[!important] 重大更新由于本人更换了 MacOS，因此目前的同步方式为 iCloud，与 Windows 的更新方式为 Github，参考 因此请酌情参考下文的内容 同步工具 我们可以参考 Obsidian 官方的文章 来查看一些同步方法，例如： 其中，Obsidian Sync 为官方的付费同步模式 [!attention] 更新注意建议使用 S3 或其他 WebDav，本人现在使用的是 iCloud + Git 的同步方法也就是把 Obsidian 的文件夹设

日常开发与实验

[!hint]这里的日常开发就不包括如何写各类公开课的实验了，最简单的方法就是使用 ，在 WSL 里随便玩，反正环境坏了也可以重装 日常开发 [!tip] 2025-10-20 更新已经换到了 MacBook Air M4 做开发，所以少了 Linux 到 Windows 的同步，但是服务器到本地的同步还是存在的，因此下面的内容也不算过时 在 MacOS 与 Linux 就可以使用 rsync -av 来做增量同步了 由于我在两台设备上进行开发，虽然都是 wsl 环境（写 C

C++ 项目初始化指北

[!tldr]在 Linux 下通过 cmake 与 Conan 进行 C++ 项目初始化与开发的一份简单指北 [!important] 重要更新其实目前也可以通过一个模板项目，例如 ModernCppStarter 来生成一个新项目，然后用 AI 帮助更改 CMakeLists.txt 即可，这种方法可能更适合新手（如果你对 AI 发出了正确清晰的命令） 环境准备 首先，我们需要下载以下软件： cmakemake 或者 ninjapython3pip 或者 pipxclan

服务器中的容器无法 ssh 连接

安装系统问题 服务器是 VMware vSphere 的一个虚拟机，开始本质上是一个 bare metal，我们需要通过 VMware 提供的工具（需要注册才能够下载）Remote Console 的文档进行下载（没有文档甚至根本不知道下载地址在哪里，太夸张了） 下载了这个之后，需要下载一个服务器 iso 文件，这里以 ubuntu-20.04.6-live-server-amd64.iso 为例。

搭建自己的 Obsidian

[!attention] 写在前面这篇文章主要讲述如何使用基础的 Obsidian 记笔记，管理知识库等，不涉及任何功能型插件；可以查看 来查看我使用的一些插件。

PicList 上传前如何压缩图像

[!danger] 注意以下的教程都建立在屏幕分辨率为 4K 的情况下，截图时会导致图像很大 截图工具 首先，我们切换截图工具，不再使用传统的 alt + ctrl + a 与 win + shift + s 我们在微软商店中下载 Snipaste，如下图所示： [!tip]如果你使用 Mac，也可以使用 HomeBrew 下载这个软件，然后将截图键设置为 Option + Q（我的设置） 这个应用能够使得截图时不已分辨率为单位，而是选中的区域多大，像素长宽就是多大，此后，我

我的科研&开发工具箱

科研&学习工具分享

创作时间

文献搜索阅读

文献搜索 这个通常没有什么好用的工具（如果 Google 算工具的话），一般是在网站上找，这里推荐几个好用的网站和一些浏览器插件 网站 出版社的官网： 好处是省事，坏处是不知道自己学校买没买版权（ 如果买了的话，可以通过 Access via Institute 来获取访问权限并下载，因为有些文章可能只能在官网上下载一些教授的主页 典型的例子：https://leria-info.univ-angers.fr/~jinkao.hao/ 甚至可以在主页上找到文章的代码/可执行文

为什么 gprof 测不准

事情的起因是我在对 SAT Solver 进行优化测试时，发现了我的求解器测不准时间，具体表现为，我在代码中测试的时间与 gprof 得到的时间不相符，后者的时间要比前者少将近 20\%，实在是让人匪夷所思。

docker 配置各类实验环境

Docker 的一些好处 使用 docker 的好处有很多，最大的特点就是你可以拿到一个速度并不算很慢，而且能够随便乱玩的 Linux 系统，而不是在自己的生产环境上乱玩。

03

根目录

📖 故事小记

这里记录一些随笔 想来想去，博客也不能全是技术文章，就放一些平时无聊写的东西上来吧 [!cite] 想成为人类 况且觉得自己在地球 Online 在线时间也上万小时了，好像也没有留下太多的痕迹，还是留下一个 NPC 的档案吧

🔗 友链

[!NOTE]排序仅按照简介中的人名/网名首字母排序 链接简介头像RSSdodoladodola (Frontend Software Engineer [at] ByteDance)https://dodolalorc.cn/rss.xmlJiangnan LiJiangnan Li (pre-Master Student [at] ISCAS, major in OMT, SMT, SAT Solving)https://blog.stevepaul101.net/ind

创作时间
04

研究&学习笔记

1 则笔记

研究&学习笔记

Claude Scholar Project KBs Active project knowledge bases now live under .

创作时间

论文阅读笔记

Boosting MCSes Enumeration

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

Improving Bit-Blasting for Nonlinear Integer Constraints

动机 前言 介绍文章前，首先需要说明对于经典的 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} 为符号位 。

Model Counting in the Wild

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

基数约束 SAT 并行策略

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

IPASIR 介绍

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

IPASIR-UP: User Propagators for CDCL

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

基数约束编码中文字顺序的重要性

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

基数约束SAT的精确求解器

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

RoundingSAT 阅读笔记其一

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

ParLS-PBO 阅读笔记

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

NuPBO 阅读笔记

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

DeciLS-PBO 阅读笔记

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

LS-PBO 阅读笔记

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

LS-ECNF 阅读笔记

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

Conflict Directed Lazy Decomposition

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

QAOA 算法

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

伪布尔优化中的分布式 QAOA 算法

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

Two-Level Segregated Fit 阅读

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

学习笔记

并行 SAT 的简单综述

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

HCP 2025 参会记录

报告 文再文 介绍的两份 LLM + OR 工作：OptMATH: ICML '25LMask林冰凯 介绍的关于 PCP 的工作金燕 介绍的两篇 ML 在 TSP 领域的应用（由于 TSP 这个问题十分契合 NLP 的各类方法，参考生物信息学）一篇强化学习做 TTP 问题一篇结合传统启发式与机器学习求解 TSP 问题，这里由于是大规模的 TSP 问题，因此我感觉文章中很多的方法其实是并行与分布式算法中常用的金耀楠 的 基于局部搜索的近线性时间图聚类算法，很早就看见这篇文章了，

MCP 协议简介

概述 [!info]更详细的内容可以访问 官网本文大部分也只是做了一部分官网内容的翻译而言（搬运工） MCP(Model Context Protocol) 是 Anthropic 在 2024 年 11 月推出的开源协议，用于将 AI 连接到外部的应用程序上，本质上是一个标准，规定了应用程序应该如何向 LLM 提供上下文。

PBO 的局部搜索求解器系列

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

NAE-SAT 的一份简单调研

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

在 ICT 学习的 MLSys

在 ICT 学习的 MLSys

这里记录了我在 ICT 的实习历程，实习的时间为 2023-06-01 到 2023-07-10 实习的内容包括两部分： 稀疏矩阵在 AI 编译器中的应用 这里，主要调研了几篇文章： 然后简单复现了一下后面两篇文章，可以参考 项目制 项目的内容需要保密，所以只能说说学习的内容，主要是学习了 的编译流程，包括如何映射到 Triton 算子的部分（但这部分本质上还不是很清晰，包括 Loop-Level IR 的 Loop 体现在什么地方）

Dynamo & Triton 解析

关于 PyTorch2.0 中对 Dynamo 的解析

SparseTIR 解读

SparseTIR 解读（论文、源码 ） Introduction 以Halide/TVM为代表的张量运算编译器，引入了计算与调度分离的概念，使得大家可以只用写一套计算描述(Tensor Expression，只与计算的数学形式有关)，用不同的调度原语(Schedule Primitive)来描述如何去优化程序(如何做矩阵分块，绑定线程，利用缓存，设计流水线，利用硬件的加速单元)，这个过程可以手动，也可以利用自动化的调度模板生成（例如 AutoTVM）并搜索，从而为不同的硬件

SparTA 解读

SparTA 解读（论文、源码 与 复现 ） Introduction 明确论文发表的时间为 2022 年，在这个时间段，算力的提升使得 DNN 的层数能够越来越深，模型越来越复杂。

SparseTIR & SparTA 环境搭建与实现复现

SparseTIR 与 SparTA 的实验复现

TVM 运行环境搭建

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

SAT 求解器

SAT 求解器

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

冲突分析与子句学习

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

相位，如何选择相位

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

SMT 基本定义

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

观察字

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

VSIDS 启发式

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

SAT 问题简介

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

05

归档文档

Obsidian 配置 Copilot 插件

[!warning] 已弃用该插件（Obsidian Copilot）已被我弃用，本文仅作存档，不再维护。

使用 Quartz 搭建博客

[!note] 已归档本笔记记录旧站（Quartz）的构建与配置，现已归档。

量子算法的预备知识

[!important]想要完全理解量子算法，还是得去阅读量子力学的内容，但在这里，主要讲解一些能够帮助快速入门量子算法的相关概念在这里，我们抛去太理论的数学公式，仅仅只是从感性上介绍相关的概念 量子计算的物理基础 [!cite]量子（Quantum）是物理学中的一个基本概念，指的是物理量的最小不可分割的基本单位，例如电子就属于量子。

PicList 上传前如何压缩图像(旧版)

[!warning] 已弃用该方案（picgo-plugin-compress-next 压缩插件）在 PicList 版本升级后已失效，本文仅作存档，不再维护。

Linux-0.11 RTFSC 环境配置

环境搭建 建议在 docker 环境下搭建，构建的 Dockerfile 如下，如果对这部分有疑问，可以参考 [!bug]如果你的位置在南方（例如香港，深圳，广州等），也就是局域网的 IP 地址为 172 或者 175 开头的，可以参考 进行解决。

2023 NENU夏令营机试题解

2023 NENU夏令营机试 Tutorial

编译原理复习

编译原理的一些简单复习

Manjaro 的安装与配置

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

2023 吉林省赛环境配置

省赛配置流程，当做遗产留下来

并查集

不相交集合数据结构(disjoint-set data structure)，简称并查集（ACM培训）

感知机与神经网络

感知机 感知机(perceptron) 是一种二分类的线性分类模型，也就是说，输入数据通过模型运算后可以输出分类的类别，由于是二分类，所以类比只有 +1, -1 我们举个例子，如果我们的输入空间是一个二维空间的话，那么感知机实际上就是找到一条直线，这条直线能把我们输入的点完全分为两个部分，如图所示： 这条直线就是感知机做的事情，下面这些红色的点，感知机将其打上标签为 -1 ，上面这些蓝色的点，感知机打上标签为 +1 标签我们可以当做是这些点的颜色，不需要觉得这是另一个维度 在

基础计算几何

基础计算几何与碰撞检测算法（蓝旭算法课）

线性回归第二讲

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

线性回归第一讲

一个传统的线性回归讲义

匈牙利算法

用以解决二分图的最大匹配（蓝旭算法课）

基础网络流

介绍一些基础的网络流算法（蓝旭算法课）

二分答案

二分答案（不是二分搜索）（蓝旭算法课）

基础加密算法

加密算法 (MD5, AES, RSA)（蓝旭算法课）

尾递归

尾递归（还是递归）（蓝旭算法课）

素数相关

这里介绍一些关于找素数的方法，可能是素数筛，也可能是快速判断一个数是不是素数

06

个人随笔

2025 年度总结

[!note]年末这一天也确实应该要写一点总结了，虽然文笔不好和流水账无异，但也算是 中关于档案的 CallBack总觉得这一年才是科研起步的第一年，但才发觉自己马上就要毕业了 2025 这年的经历算是大学+研究生六年来最丰富的一年了，想来在未来的很多年都会记得这一年的经历。

保研苦旅

[!info]文章的内容都写于 2023.9.29把这篇文章从备忘录里搬出来的时候我的研究生生活已经快结束了，没想到在这个时间点再次面临三年前的同样的境况但看来我依旧没有什么成长 写在前面 想到要写这篇文章的时候，正坐在前往北京的高铁上，急着去参加一场可能并不存在的面试。

01-Japan

1 则笔记

大阪 (Osaka)-Day1-出境

上海浦东出境 [!info]由于 1 号下午还要开会，所以 31 号晚上一夜没睡，一直在忙着写代码跑实验，期望开会前能多做点东西，毕竟要给自己放假了（ 进机场的时候没拍什么照片，全称在看小红书教程，毕竟是第一次出国，完全不知道应该要干什么，办理完托运就急急忙忙地扫码注册 Visit Japan Web 的账号，说是到日本会有用。

笔记
↑ ↓ 选择↵ 打开Esc 关闭