# HUST-2022-PROGRAM

**Repository Path**: xiao-mingyu/HUST-2022-PROGRAM

## Basic Information

- **Project Name**: HUST-2022-PROGRAM
- **Description**: No description available
- **Primary Language**: Unknown
- **License**: Not specified
- **Default Branch**: main
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 0
- **Forks**: 0
- **Created**: 2026-03-21
- **Last Updated**: 2026-03-21

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

本设计基于 *DPLL* 的算法与程序框架，实现一个完备 *SAT* 求解器，同时程序的改进，对输入的 *CNF* 范式算例文件，解析并建立其内部表示；精心设计问题中变元、文字、子句、公式等有效的物理存储结构，设计分支变元处理策略， 使求解器具有优化的执行性能；对一定规模的算例能有效求解，输出与文件保存求解结果，统计求解时间。

数独游戏可转化为 *SAT* 问题，用本系统实现的 *SAT* 求解器可以快捷地对数独问题转化的 *CNF* 文件进行求解，再以变元真值数据转化的数独盘格式输出求解答案。本系统具有一定的交互功能，用户可以利用本系统进行数独游戏，系统将自动判断解的正确性，并输出正确答案。

### 具体研究工程步骤如下：

1. 对于 *SAT* 求解问题的相关背景、基本原理以及传统的 *DPLL* 框架进行深入了解，根据相关资料对于项目确定整体方向，设计项目整体流程。
2.   根据 *SAT* 求解器设计相应的数据结构和算法，进而实现基于 *DPLL* 框架的 *SAT* 求解器，并使用相应的算例进行测试:
   -  数据结构主要使用十字链表的结构
   -   *CNF* 文件的读取、解析和初始化
   - 基于 *DPLL* 框架的 *SAT* 求解器（核心模块）
   - 双数独问题的生成和归约，转化成 *SAT* 问题并求解
3.  通过查阅文献和不断尝试，优化数据结构和算法，实现求解效率的提高。主要优化方向有：
   - 数据结构优化
   -  变元分支选取策略优化
   - 算法框架优化
4. 设计问题转化策略将数独问题归约为 *SAT* 问题并求解。
5. 在程序实现的过程中将程序各个结构模块化