[VLSI CAD] MiniSAT？

满意度 (SAT) 问题可概括为以下问题：

变量能否设置为真/假，从而使给定的布尔公式为真？

例如，给定公式 f(x,y,z)=(x || y) & (!x || z)，

• 找出如何为 x、y 和 z 赋值为 True/False，从而使整个公式为 True，这就是一个 SAT 问题。

这看起来很简单，但是当变量的数量达到数千或数万时，

• 而约束条件达到数十万时，
• 就变得完全探索不可能了。

迷你卫星页面

by Niklas Eén, Niklas Sörensson

2.MiniSat 是一种什么样的 SAT 求解器

MiniSat 是一种基于 CDCL 的高性能 SAT 求解器。

特点包括：

• CDCL（冲突驱动条款学习）
• 代码库非常小
• 快速、稳定
• 易于作为库嵌入到其他工具中

因此，虽然 MiniSat 可以单独使用，但它实际上更常用于以下方面。

• 规范验证工具内部引擎
• EDA 工具决策引擎
• 研究原型基线求解器
• SMT/PB 求解器后台 SAT 引擎

例如

MiniSat 更像是 "SAT 求解器领域的标准引擎"

3.

例如，这个约束不是 SAT：

3a + 2b + c ≥ 4

在这里，a、b 和 c 是布尔变量，但表达式本身是一个具有整数权重的 约束。

这种约束被称为伪布尔（PB）约束。

PB 问题的特点是：

• 变量是布尔的
• 约束条件是线性整数不等式
• 通常有一个优化问题（最小/最大）

4.MiniSat+ 的核心理念

MiniSat+ 并不是一个新的求解器。<它只有一个核心思想：

将 PB 约束翻译成 SAT，然后用 MiniSat 求解

结构如下：

PB 问题
↓ （翻译）
SAT 问题
↓
MiniSat

MiniSat+ 负责这个翻译层。

5. 如何将 PB → SAT 转换为 SAT

MiniSat+ 使用以下基于逻辑电路的技术将 PB 约束转换为 SAT。

• BDD（二元判定图）
• 加法网络
• 排序网络

关键在于：

• 创建一个 逻辑电路
• 确定是否满足 PB 约束
• 使用 Tseitin 转换将电路转换为 CNF
• 将结果输入 MiniSat

即、

"Create a circuit that checks for constraints,

6.为什么要改用 SAT

您可能会问，为什么不编写自己的 PB 解算器呢？

• 数十年来，SAT 求解器一直在不断优化
• 条款学习、启发式、传播都非常强大
• 对于 "几乎是 SAT 的问题"，
  • SAT 转换 + MiniSat 通常比 PB 本地求解器更快
    • 大多是布尔结构
    • 只有一些权重/计数约束
  • Formal equivalence checking
  • Selecting a minimal fix set in ECO
  • Constraint-based synthesis
  • Resource / option selection problems
  • Some STA/CDC/DFT internal decision logic
  • MiniSat
    → 高性能布尔 SAT 求解器
    → 用于求解选择问题的快速引擎
  • MiniSat+
    → SAT 的整数加权约束 (PB)。利用 MiniSat 的强大功能
  • 为什么使用它
    → SAT 求解器仍然是最强大的组合搜索引擎
    → 结构上非常适合 EDA/验证

尤其是对于 EDA/验证问题：MiniSat+ 方法在这些结构上运行良好。

7. 从 EDA 角度看它的用途

从工程师的角度看，MiniSat 系列非常适合解决以下问题。它们的共同点是都具有这个特点。

选择变量 + 约束条件 + 组合爆炸

一旦您尝试用人工逻辑手动处理这些问题，就会成为维护工作的噩梦。

8.一段摘要

。