SATNet:使用可区分的可满足性求解器桥接深度学习和逻辑推理-源码

SATNet• 使用可区分的可满足性求解器桥接深度学习和逻辑推理。 这个软件库包含源代码重现实验中ICML 2019纸由， ，和。 什么是SATNet SATNet是可微分（平滑）的最大可满足性（MAXSAT）求解器，可以集成到较大的深度学习系统的循环中。 该（近似）求解器基于快速坐标下降法来求解与MAXSAT问题相关的半定程序（SDP）。 SATNet如何运作 SATNet层将已知MAXSAT变量的离散或概率分配作为输入，并通过权重为S的MAXSAT SDP弛豫输出未知变量的分配猜测。 下图显示了该层正向通过的示意图。 为了获得后向通行证，我们通过SDP松弛来进行分析区别（有关更多详细信息，请参见本文）。 实验概述 我们表明，通过将SATNet集成到端到端学习系统中，我们可以以最少的监督方式学习挑战性问题的逻辑结构。 特别是，我们表明我们可以： 使用单比特监督学习奇偶校验功能（传