第七节课作业：基于神经网络的SAT问题求解

问题描述

SAT（布尔可满足性）问题是第一个被证明为NP完全的问题，传统求解方法主要基于回溯搜索和冲突分析。本作业探讨如何使用机器学习和神经网络方法来求解SAT问题，重点分析其输入输出设计和数据集构建。

1. 神经网络输入输出设计

1.1 输入表示方法

方法一：矩阵编码表示

[ 1  -1   1 ]
[-1   1   0 ]
[ 0   1  -1 ]

方法二：图结构表示

• 二分图：变量节点和子句节点
• 边连接：表示变量与子句的包含关系
• 边权重：区分正负文字（+1/-1）

方法三：序列化表示

• 子句序列：将每个子句转换为固定长度的向量
• 位置编码：添加位置信息

1.2 输出表示方法

输出类型一：变量赋值预测

输出类型二：可满足性分类

输出类型三：决策序列

2. 训练数据集构建

2.1 数据生成策略

随机SAT实例生成

参数设置：
- n: 变量数量 (10-1000)
- m: 子句数量
- k: 每个子句文字数量 (通常k=3)
- α = m/n: 子句密度

生成算法：
1. 随机选择k个不同的变量
2. 随机决定每个变量的正负
3. 组合成子句
4. 重复m次得到CNF公式

难度分级数据集

2.2 标签获取方法

使用传统SAT求解器

• 求解器选择：MiniSat、Glucose等现有求解器
• 输出标签：
  • 变量赋值：满足公式的具体解
  • 可满足性：SAT/UNSAT标签
  • 求解时间：难度指标

标签格式

{
  "formula_id": "sat_001",
  "variables": 50,
  "clauses": 200,
  "sat": true,
  "assignment": [1, 0, 1, 1, 0, ...],
  "solving_time": 0.025
}

2.3 数据增强技术

对称性增强

• 变量重命名：随机排列变量顺序
• 子句重排序：随机打乱子句顺序
• 符号翻转：统一翻转变量符号

噪声增强

• 子句删除：随机删除部分冗余子句
• 子句添加：添加可推导的冗余子句

3. 数据集实例示例

3.1 简单3-SAT实例

[ 1  1 -1]
[-1  1  0]
[ 0 -1  1]
[ 1  0  1]

3.2 不可满足实例

[ 1  0]
[ 0  1]
[-1  0]
[ 0 -1]

4. 数据集规模建议

4.1 训练集规模

4.2 测试集分布

• 同规模测试：与训练集相同变量数
• 跨规模测试：训练50变量，测试100变量
• 跨难度测试：不同α值的公式

5. 评估指标

5.1 分类指标

• 可满足性准确率：SAT/UNSAT分类正确率
• 精确率/召回率：针对SAT或UNSAT类别

5.2 赋值指标

• 变量赋值准确率：单个变量预测正确率
• 完全正确率：所有变量都预测正确的比例
• 汉明距离：预测赋值与真实赋值的差异

6. 神经网络架构建议

6.1 基于CNN的架构

class SATSolverCNN(nn.Module):
    def __init__(self, n_vars, n_clauses):
        super().__init__()
        self.conv1 = nn.Conv2d(1, 32, kernel_size=3, padding=1)
        self.conv2 = nn.Conv2d(32, 64, kernel_size=3, padding=1)
        self.fc1 = nn.Linear(64 * n_clauses * n_vars, 256)
        self.fc2 = nn.Linear(256, n_vars)  # 输出每个变量的赋值
        
    def forward(self, x):
        # x: [batch, 1, n_clauses, n_vars]
        x = F.relu(self.conv1(x))
        x = F.relu(self.conv2(x))
        x = x.view(x.size(0), -1)
        x = F.relu(self.fc1(x))
        x = torch.sigmoid(self.fc2(x))  # 输出概率
        return x

6.2 基于GNN的架构

class SATSolverGNN(nn.Module):
    def __init__(self, n_vars, hidden_dim=64):
        super().__init__()
        self.var_embedding = nn.Embedding(n_vars, hidden_dim)
        self.gnn_layers = nn.ModuleList([
            GCNConv(hidden_dim, hidden_dim) for _ in range(3)
        ])
        self.output = nn.Linear(hidden_dim, 1)
        
    def forward(self, edge_index, edge_attr):
        # 图神经网络处理变量-子句图
        x = self.var_embedding.weight
        for layer in self.gnn_layers:
            x = F.relu(layer(x, edge_index, edge_attr))
        return torch.sigmoid(self.output(x))