LinSATNet: The Positive Linear Satisfiability Neural Networks

将约束条件编码到神经网络中非常有吸引力。本文研究了如何将流行的正线性可满足性引入神经网络中。我们提出了第一个可微分的可满足性层，基于经典Sinkhorn算法的扩展，用于联合编码多组边际分布。我们进一步理论地表征了Sinkhorn算法在多个边际分布上的收敛性质。与顺序决策（例如基于强化学习的求解器）相比，我们展示了我们的技术在通过一次神经网络解决受约束（特别是可满足性）问题方面的应用，包括：i）一个神经路由求解器，不需要最优解的监督学习；ii）一个处理两侧均存在无法匹配的离群点的部分图匹配网络；iii）一个用于具有连续约束的金融投资组合的预测网络。据我们所知，在将这些情况表述为可满足性问题时，不存在一次性神经求解器。源代码可在 https://github.com/Thinklab-SJTU/LinSATNet 获取。

本文旨在将正线性可满足性引入神经网络中，提出了一种可微分的满足性层，并应用于解决多种约束问题，包括路由问题、图匹配问题和金融投资组合优化问题等。

本文提出了一种基于Sinkhorn算法的不同iable满足性层，用于联合编码多组边缘分布，并对多个边缘分布的Sinkhorn算法的收敛性进行了理论分析。相比于基于顺序决策的强化学习等算法，本文提出的方法可以实现一次性神经网络求解满足性问题。

本文提出的方法在三个具体问题上进行了实验验证：一是无监督学习的神经路由求解器，二是处理存在不匹配异常值的图匹配网络，三是金融投资组合的预测网络。实验结果表明，本文提出的方法在这些问题上具有较好的性能。此外，本文提供了开源代码，方便其他研究者进行相关研究。

在相关研究方面，最近也有一些研究关注于将约束引入神经网络中，例如基于深度强化学习的约束求解器等。