L'intégration de la raisonnement logique au sein des architectures d'apprentissage profond est un objectif majeur des systèmes d'IA modernes. Dans cet article, nous proposons une nouvelle orientation vers cet objectif en introduisant un solveur de satisfiabilité maximale (MAXSAT) différentiable (lissé) qui peut être intégré dans la boucle de systèmes d'apprentissage profond plus vastes. Notre solveur (approximatif) repose sur une approche rapide de descente coordonnée pour résoudre le programme semi-défini (SDP) associé au problème MAXSAT. Nous montrons comment dériver analytiquement à travers la solution de ce SDP et résoudre efficacement la passe arrière associée. Nous démontrons que l'intégration de ce solveur dans des systèmes d'apprentissage end-to-end permet d'apprendre la structure logique de problèmes difficiles avec une supervision minimale. En particulier, nous montrons que nous pouvons apprendre la fonction parité en utilisant une supervision à un bit (une tâche traditionnellement difficile pour les réseaux profonds) et apprendre à jouer au Sudoku 9x9 uniquement à partir d'exemples. Nous résolvons également un problème de « Sudoku visuel » qui associe des images de grilles de Sudoku à leurs solutions logiques correspondantes en combinant notre solveur MAXSAT avec une architecture convolutive traditionnelle. Notre approche montre donc un potentiel prometteur pour l'intégration de structures logiques dans l'apprentissage profond.