QtSAT

图形界面的布尔可满足性问题（SAT）求解器，集成了 PicoSAT 。

项目简介

布尔可满足性问题（Boolean satisfiability problem）是判定是否存在使布尔公式为真的变量赋值的NP完全问题，由斯蒂芬·库克（1971年）和列昂尼德·莱文（1973年）分别独立证明其为NP完全问题，是第一个被证明的NP完全问题。其基本形式要求检查命题逻辑公式是否可通过变量赋值得到真值结果。

QtSAT 是一个使用 Qt 框架开发的图形化 SAT 求解器，集成了 PicoSAT 库作为核心求解引擎。用户可以通过友好的界面输入逻辑子句，求解器会自动计算并展示所有满足条件的解。

功能特性

• 图形化界面：直观的子句输入界面和结果展示
• 多解枚举：支持求解多个满足条件的解（最多 10 个）
• 中文界面：全中文操作界面，易于理解和使用
• 输入验证：自动验证子句输入格式，提供详细的错误提示

输入格式

范式存在定理（Existence Theorem of Normal Form）表明命题演算中任一合式公式A，恒可表示为等值的合取范式或析取范式。一公式和它的范式等值。置换不改变公式的真值，因而通过置换可以把一公式变换为一范式。这一定程度上说明了对于标准形命题公式的研究的一般性。

合取范式（Conjunctive Normal Formula，CNF），是命题公式的一种标准形。若干个析取项的合取称为一个合取范式。PicoSAT强制要求CNF输入，是为了统一输入标准，让求解器能更高效地处理SAT问题（布尔可满足性问题），带来高效的实现。

子句语法

问题表述通过CNF。可以输入多个子句，每个子句支持：

• 变量：由字母组成（如 A、B、C、abc）
• 逻辑或：使用 || 表示
• 逻辑非：使用 ! 表示

每个子句之间是合取（&&）。

示例

A || B
!A || !B

表示逻辑公式：(A ∨ B) ∧ (¬A ∨ ¬B)

项目结构

qtSAT/
├── PicoSAT/           # PicoSAT 求解器库
│   ├── LICENSE        # 许可证文件
│   ├── picosat.c      # PicoSAT 核心实现
│   ├── picosat.h      # PicoSAT 头文件
│   └── version.c      # 版本信息
├── QtSAT.pro          # Qt 项目文件
├── QtSATMainWindow.cpp# 主窗口实现
├── QtSATMainWindow.h  # 主窗口头文件
├── QtSATMainWindow.ui # 界面设计文件
├── main.cpp           # 程序入口
└── README.md          # 项目说明

构建与运行

环境要求

• Qt 5.14.2 或更高版本

构建步骤

1. 使用 Qt Creator 打开 QtSAT.pro 文件
2. 选择构建配置（Release 或 Debug）
3. 点击构建按钮

使用说明

1. 添加子句：在输入框中输入子句（如 A || B），点击「添加子句」按钮
2. 管理子句：
   • 选中子句后点击「删除选中」可删除单条子句
   • 点击「清空全部」可删除所有子句
3. 求解：点击「求解」按钮，求解器会计算所有满足条件的解
4. 查看结果：求解结果会显示在右侧面板中

界面截图

技术实现

核心组件

• QtSATMainWindow：主窗口类，负责界面交互和求解逻辑
• PicoSAT：SAT 求解器核心库

求解流程

1. 用户输入子句
2. refineClause() 函数解析和验证子句格式
3. parseClause() 函数将子句转换为整数表示
4. 调用 PicoSAT 库进行求解
5. solveMultipleSAT() 函数枚举多个解
6. 显示求解结果

相关应用

现在的软件系统除了内置SAT求解器，还带有领域相关的描述语言，且通过图形界面将问题转换为SAT求解器的输入，获得求解的成果，直接输入SAT子句的较少。QtSAT以简单的界面集成PicoSAT求解器，可以便于了解SAT问题相关的环节。

这些是一些经典的实际应用：

• 集成电路正式验证：将芯片设计与其规格模型编码为布尔公式，若公式可满足则找到导致输出差异的输入（即设计缺陷），若不可满足则证明两者功能等价。这是EDA工具中等价性检查的核心技术，用于发现CPU、GPU等芯片中的逻辑错误。

• 软件与系统验证：把“系统在有限步内进入错误状态（如死锁、缓冲区溢出）”转化为布尔公式。可满足时给出具体的错误执行路径，帮助开发者复现漏洞；不可满足则证明系统在该步数内安全。常用于飞机飞控、银行交易系统、操作系统驱动的正确性证明。

• 自动规划与调度：设定时间步长上限，用布尔变量表示各时刻的状态和动作，编码初始条件、目标状态与操作约束。若公式可满足，求解出的赋值直接对应一个有效操作序列。应用包括物流车辆路径规划、火星车任务调度、游戏AI步骤求解。

• 自动测试向量生成（ATPG）：判断是否存在输入信号能检测芯片内部的固定故障（如某节点恒为0或1）。SAT求解器若返回可满足，该输入即为有效测试向量，可被自动测试设备用于筛选制造缺陷的芯片。

• 逻辑综合与优化：判断两个逻辑表达式是否等价，或某逻辑门是否冗余。通过构造SAT公式，若不可满足则说明移除该门不影响电路功能，从而实现芯片面积和功耗的优化。

• 组合设计与谜题求解：将数独、N皇后、图着色、扫雷等谜题的规则编码为布尔子句，交给SAT求解器。例如，数独中每个格子填数字的条件可表示为逻辑变量，求解器能在毫秒级解出最难的题目。

• 密码分析：将加密算法（如简化版AES、流密码）转换为布尔公式，以已知明密文对为固定条件，密钥位为自由变量。求解器尝试找出正确密钥，用于评估轻量级密码的安全性。但对完整强密码（如标准AES）通常因规模过大而不可行。

参考文献

• Propositional Logic
• The Mathematics of Boolean Algebra
• PicoSAT - SAT 求解器库
• Qt Framework - 跨平台应用框架