最近更新

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

为什么选择 chezmoi 管配置、mpm 登记软件，以及这套仓库的使用方式与自动化搭建过程

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

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

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

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

[!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 只要求找到有多少组满足公式

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

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

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

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

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

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

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

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

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

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

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

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

[!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 并行求解策略主要分为两类：分治法以及基于组合策略的并行。

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

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

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

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

这里记录了本科时期（以及后来）写的一些学习博客，由于可能很久都不会再回顾了所以放在这里 目录可以参考

这里收录了我在 csdiy 上学习的一系列公开实验（当然，也有一部分不在这个网站上收录），每门课也对应一个 #主题/ 标签，方便按主题归档 基础工具 这部分课程会教会你，CS 系的学生如何使用电脑，当然，鉴于大家的电脑大多都还是 Windows，我推荐首先阅读 来试试看 WSL。

研究论文阅读与笔记整理

这里记录了我的文具袋系列，会写一些遇到的各种环境问题，推荐一些工具，以及分享我使用的开发工具与工作流等 📝 开发环境配置 主要是配置一些公开课实验的环境，或者对个人而言开发更方便的环境，这部分内容可以在 #主题/环境配置 中查看 或者也会记录遇到的一些奇怪的问题（但这种或许只和我自己的环境相关，并不保证可复现性），这部分可以参考 #主题/故障排查 🔧 工具推荐 这里主要推荐一些我使用的工具，例如一些 VSCode 的插件/代码编辑器/AI 等等，全部的文章可以通过下方的标

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

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

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

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

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

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

起因 我们有以下代码： 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

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

[!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 有关的问题。

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

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

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

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

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

SparseTIR 与 SparTA 的实验复现

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

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

关于 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

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

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

如何从 X11 转向 Wayland 下的配置

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

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

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

2023 NENU夏令营机试 Tutorial

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

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

实验准备 只针对 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 的内容是简单的熟悉 xv6 操作系统和怎么做实验，官网上对实验难度的描述是easy , easy, moderate/hard, moderate, moderate。

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

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

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

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

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

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

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

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

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

科研&学习工具分享

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

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

一个传统的线性回归讲义

Set the envrionment and boot the machine

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

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

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

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

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

编译原理的一些简单复习

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

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

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

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

关于 PyTorch2.0 中对 Dynamo 的解析

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

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

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

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

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

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