利用可微可满足性求解器实现深度学习与逻辑推理的衔接
satnet的Python项目详细描述
卫星网络•
使用可微可满足性求解器将深度学习和逻辑推理连接起来。
此存储库包含源代码，用于通过Po-Wei Wang、Priya L. Donti、Bryan Wilder和J. Zico Kolter在ICML2019论文SATNet: Bridging deep learning and logical reasoning using a differentiable satisfiability solver中复制实验。
什么是satnet
SATNet是一个可分（平滑）最大可满足性（Max SAT）求解器，它可以被集成到更大的深度学习系统的回路中。这个（近似）解算器是基于快速坐标下降法求解与Max SAT问题相关的半定程序（SDP）。
卫星网络的工作原理
satnet层以已知maxsat变量的离散或概率赋值为输入，通过maxsat-sdp松弛输出未知变量赋值的猜测，其权值为s。下面显示了描述该层正向通过的示意图。为了得到后向通道，我们通过sdp松弛进行解析微分（详见论文）。
实验概述
我们证明，通过将satnet集成到端到端学习系统中，我们可以以最小监督的方式学习具有挑战性的问题的逻辑结构。特别是，我们可以：
- 学习奇偶校验函数使用单位监督（对于深层网络来说，这是一项传统的艰巨任务）
- 仅从示例中学习如何玩9×9数独（原创和排列）。
- 解决一个“视觉数独”问题，该问题将数独谜题的图像映射到相关的逻辑解决方案。（下面显示了一个“视觉数独”输入示例。）
安装
通过PIP
pip install satnet
来源
git clone https://github.com/locuslab/SATNet cd SATNet && python setup.py install
包依赖关系
conda install -c pytorch tqdm
通过Docker图像
cd docker
sh ./build.sh
sh ./run.sh
运行实验
jupyter笔记本和google colab
Jupyter notebook 以及Google Colab
手动运行它们
获取数据集
可以通过
下载Sudoku dataset和Parity datasetwget -cq powei.tw/sudoku.zip && unzip -qq sudoku.zip wget -cq powei.tw/parity.zip && unzip -qq parity.zip
数独实验（原始、排列和视觉）
python exps/sudoku.py python exps/sudoku.py --perm python exps/sudoku.py --mnist --batchSz=50
奇偶性实验
python exps/parity.py --seq=20 python exps/parity.py --seq=40
欢迎加入QQ群-->： 979659372
