  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.
