Abstract
Integrating logical reasoning within deep learning architectures has been amajor goal of modern AI systems. In this paper, we propose a new directiontoward this goal by introducing a differentiable (smoothed) maximumsatisfiability (MAXSAT) solver that can be integrated into the loop of largerdeep learning systems. Our (approximate) solver is based upon a fast coordinatedescent approach to solving the semidefinite program (SDP) associated with theMAXSAT problem. We show how to analytically differentiate through the solutionto this SDP and efficiently solve the associated backward pass. We demonstratethat by integrating this solver into end-to-end learning systems, we can learnthe logical structure of challenging problems in a minimally supervisedfashion. In particular, we show that we can learn the parity function usingsingle-bit supervision (a traditionally hard task for deep networks) and learnhow to play 9x9 Sudoku solely from examples. We also solve a "visual Sudok"problem that maps images of Sudoku puzzles to their associated logicalsolutions by combining our MAXSAT solver with a traditional convolutionalarchitecture. Our approach thus shows promise in integrating logical structureswithin deep learning.