Prédire la satisfiabilité propositionnelle par l'apprentissage de bout en bout

Curieusement, il est possible d'utiliser des modèles d'apprentissage automatique pour prédire le statut de satisfiabilité de problèmes SAT difficiles avec une précision bien supérieure à celle d'une estimation aléatoire. Les méthodes existantes s'appuient sur une ingénierie manuelle approfondie des caractéristiques et sur des caractéristiques complexes sur le plan informatique (par exemple, basées sur des relaxations de programmation linéaire). Nous montrons pour la première fois qu'il est possible d'obtenir des performances encore meilleures avec des méthodes d'apprentissage de bout en bout, c'est-à-dire des modèles qui passent directement des données brutes du problème aux prédictions et dont l'évaluation ne prend qu'un temps linéaire. Notre travail s'appuie sur des modèles de réseaux profonds qui capturent une invariance clé des problèmes SAT : le statut de satisfiabilité n'est pas affecté par la réorganisation des variables et des clauses. Nous avons montré que l'apprentissage de bout en bout avec des réseaux profonds peut surpasser les travaux précédents sur des problèmes 3-SAT aléatoires à la transition de phase de solubilité, où : (1) exactement 50 % des problèmes sont satisfaisables ; et (2) les temps d'exécution empiriques des méthodes de résolution connues évoluent de façon exponentielle avec la taille du problème (par exemple, nous avons obtenu une précision de prédiction de 84 % sur des problèmes à 600 variables, qui prennent des heures à résoudre avec les méthodes de pointe). Nous avons également montré que les réseaux profonds peuvent se généraliser en fonction de la taille des problèmes (par exemple, un réseau entraîné uniquement sur des problèmes à 100 variables, qui prennent généralement environ 10 ms à résoudre, a atteint une précision de 81 % sur des problèmes à 600 variables).

Remerciements
Ces travaux ont tiré parti des ressources informatiques fournies par Calcul Canada, la FCI, le BCKDF et NVIDIA ; ils ont été financés par une subvention à la découverte du CRSNG, un supplément de subvention à la découverte du MDN/CRSNG, une chaire de recherche en IA du CIRC (Alberta Machine Intelligence Institute) et la bourse FA8750- 19-2-0222 du DARPA, CFDA #12.910 (Air Force Research Laboratory).