Boosting MCSes Enumeration文章链接 本文提出了一种基于**转移子句（Transition Clause）与递归模型旋转（Recursive Model Rotation, rmr）**的 MCS 枚举加速技术。
Improving Bit-Blasting for Nonlinear Integer Constraints介绍文章前，首先需要说明对于经典的 SMT(QF_NIA)，基于 bit-blasting 做法，简而言之主要是以下三步：
Model Counting in the WildPropositional Model Counting (MC) 即命题模型计数（\sharpSAT）是计算一个 CNF 公式 \mathcal{F} 中有多少个解（即 model）
通过 submodule 发布博客由于在 Obsidian 中，虽然我有不被 git 追踪的文件夹（私有文件夹），但是这也限制了我多设备同步 的需求（因为 Windows 上的 iCloud 十分难用）
使用 Quartz 搭建博客关于官方的构建教程，可以参考：quartz 官方文档，如果看不习惯英文，也可以参考 quartz 文档中文版，但需要注意的是中文文档有些过时了，有很多新的 Features 都没有翻译
MacOS 软件推荐这里可能需要绕一下，如果你使用 brew 安装了 fish，首先打开终端，输入 fish 后启动 然后，输入 which fish 拿到路径，例如 /opt/homebrew/bin/fish 将这个…
服务器中的容器无法 ssh 连接服务器是 VMware vSphere 的一个虚拟机，开始本质上是一个 bare metal，我们需要通过 VMware 提供的工具（需要注册才能够下载）Remote Console 的文档进行下载（…
SMT 基本定义在 SAT 中，我们引入了命题逻辑（Propositional Logic）来编码与表达现实问题，但我们知道，Propositional Logic 的表达能力本质上并不是很强，对于一些复杂的问题，我…
MCP 协议简介MCP(Model Context Protocol) 是 Anthropic 在 2024 年 11 月推出的开源协议，用于将 AI 连接到外部的应用程序上，本质上是一个标准，规定了应用程序应该如何…
Conflict Directed Lazy Decomposition文章链接 在 SAT 问题的全局约束中，如果将约束编码为 SAT，会导致变量与子句的急速膨胀，造成求解困难。但有时候，编码的辅助变量又属于 nogood 类型的变量，能够指导搜索的过程。
QAOA 算法文章链接 对于一个哈密顿量，我们总可以把它拆成若干部分之和： 又根据含时哈密顿量在薛定谔方程中的解，我们可以得出 U(H, t) = \exp{(\frac{-iHt}{\hbar})} 根据 Tro…
DeciLS-PBO 阅读笔记文章链接 与 代码链接 本文和 NuPBO CP'23 是同年的文章，因此没有对比，这篇文章的 实验效果 看了一下是不如 NuPBO 的效果 的，尤其是 300s 中 MWCB 和 SAP，NuPBO…
LS-PBO 阅读笔记文章链接 提出了一种局部搜索求解 PBO 的框架，主要的思路就是把优化转为判定，由此可以使用 SAT 局部搜索求解器的思路，通过对约束加权（惩罚值），并由此进行打分函数的设计，从而指导启发式算法工作…
LS-ECNF 阅读笔记文章链接 本文提出了一种针对 局部 基数约束的局部搜索算法 LS-ECNF ，通过 ECNF 的形式，可以避免将基数约束编码为 SAT，从而获取更好的求解性能 本文的后续改进为 LS-PBO SAT'…
文献搜索阅读Your personal research assistant Zotero is a free, easy-to-use tool to help you collect, organize, a…
SparTA 解读明确论文发表的时间为 2022 年，在这个时间段，算力的提升使得 DNN 的层数能够越来越深，模型越来越复杂。此时，为了提高 DNN 效率而必须进行稀疏化，也就是尽可能地减少不必要的数据冗余。