# Learning Reliable Logical Rules with SATNet

arXiv: https://arxiv.org/abs/2310.02133 · HTML: https://mlsanity.com/paper/2310.02133/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 23 of its 39 references that are in the map.
- First posted on arXiv 3 Oct 2023.

## Placed in

- LLM reasoning / [Reasoning benchmarks and evaluation](https://mlsanity.com/lr/reasoning-benchmarks-and-evaluation/)

## Builds on (most cited first, 23 of 23)

- [OptNet: Differentiable Optimization as a Layer in Neural Networks](https://mlsanity.com/paper/1703.00443/) (2017)
- [Interaction Networks for Learning about Objects, Relations and Physics](https://mlsanity.com/paper/1612.00222/) (2016)
- [Neural Probabilistic Logic Programming in DeepProbLog](https://mlsanity.com/paper/1907.08194/) (2019)
- [A simple neural network module for relational reasoning](https://mlsanity.com/paper/1706.01427/) (2017)
- [Learning Explanatory Rules from Noisy Data](https://mlsanity.com/paper/1711.04574/) (2017)
- [Fast Differentiable Sorting and Ranking](https://mlsanity.com/paper/2002.08871/) (2020)
- [DRUM: End-To-End Differentiable Rule Mining On Knowledge Graphs](https://mlsanity.com/paper/1911.00055/) (2019)
- [SATNet: Bridging deep learning and logical reasoning using a differentiable satisfiability solver](https://mlsanity.com/paper/1905.12149/) (2019)
- [End-to-End Differentiable Proving](https://mlsanity.com/paper/1705.11040/) (2017)
- [Neural Logic Machines](https://mlsanity.com/paper/1904.11694/) (2019)
- [NeurASP: Embracing Neural Networks into Answer Set Programming](https://mlsanity.com/paper/2307.07700/) (2023)
- [Recurrent Relational Networks](https://mlsanity.com/paper/1711.08028/) (2017)
- [Neural Logic Reinforcement Learning](https://mlsanity.com/paper/1904.10729/) (2019)
- [Neural-Symbolic Integration: A Compositional Perspective](https://mlsanity.com/paper/2010.11926/) (2020)
- [Learn to Explain Efficiently via Neural Logic Inductive Learning](https://mlsanity.com/paper/1910.02481/) (2019)
- [Techniques for Symbol Grounding with SATNet](https://mlsanity.com/paper/2106.11072/) (2021)
- [Learning to Solve Constraint Satisfaction Problems with Recurrent Transformer](https://mlsanity.com/paper/2307.04895/) (2023)
- [The Mixing method: low-rank coordinate descent for semidefinite programming with diagonal constraints](https://mlsanity.com/paper/1706.00476/) (2017)
- [DeepLogic: Towards End-to-End Differentiable Logical Reasoning](https://mlsanity.com/paper/1805.07433/) (2018)
- [Low-rank semidefinite programming for the MAX2SAT problem](https://mlsanity.com/paper/1812.06362/) (2018)
- [Diff-Explainer: Differentiable Convex Optimization for Explainable Multi-hop Inference](https://mlsanity.com/paper/2105.03417/) (2021)
- [Learning Symmetric Rules with SATNet](https://mlsanity.com/paper/2206.13998/) (2022)
- [An Integer Linear Programming Framework for Mining Constraints from Data](https://mlsanity.com/paper/2006.10836/) (2020)

## Built on by (most cited first, 3 of 3)

- [LogiCity: Advancing Neuro-Symbolic AI with Abstract Urban Simulation](https://mlsanity.com/paper/2411.00773/) (2024)
- [Learning Minimal Neural Specifications](https://mlsanity.com/paper/2404.04662/) (2024)
- [Scaling Neuro-symbolic Problem Solving: Solver-Free Learning of Constraints and Objectives](https://mlsanity.com/paper/2508.20978/) (2025)

## Abstract (arXiv)

Bridging logical reasoning and deep learning is crucial for advanced AI systems. In this work, we present a new framework that addresses this goal by generating interpretable and verifiable logical rules through differentiable learning, without relying on pre-specified logical structures. Our approach builds upon SATNet, a differentiable MaxSAT solver that learns the underlying rules from input-output examples. Despite its efficacy, the learned weights in SATNet are not straightforwardly interpretable, failing to produce human-readable rules. To address this, we propose a novel specification method called "maximum equality", which enables the interchangeability between the learned weights of SATNet and a set of propositional logical rules in weighted MaxSAT form. With the decoded weighted MaxSAT formula, we further introduce several effective verification techniques to validate it against the ground truth rules. Experiments on stream transformations and Sudoku problems show that our decoded rules are highly reliable: using exact solvers on them could achieve 100% accuracy, whereas the original SATNet fails to give correct solutions in many cases. Furthermore, we formally verify that our decoded logical rules are functionally equivalent to the ground truth ones.