Il s’agit de transformer un problème linéaire en nombres entiers avec paramètres, en un problème équivalent SAT.
La résolution de problèmes entiers paramétriques linéaires se retrouve au cœur de la parallélisation des entraînements actuellement pour de grands modèles de langage (Large Language Models) [7]. C’est une étape importante de l’optimisation, qui s’appuie notamment sur quelques solveurs linéaires entiers et paramétriques. Basés sur l’algorithme du simplexe et sur des coupes pour ne retenir que les solutions entières, ces méthodes sont très coûteuses ont fait l’objet de nombreux travaux proposant des alternatives pour la parallélisation [2,3,4]. Les méthodes théoriques ont peu évolué récemment. A l’opposé, des méthodes de résolution SAT testant la satisfiabilité de clauses conjonctives/disjonctives de variables booléennes ont bénéficié récemment d’heuristiques permettant une accélération importante.
L’objectif de ce sujet est de transformer un problème linéaire en nombres entiers, avec paramètres, en un problème équivalent SAT et tester son temps de résolution avec les deux méthodes. Le codage d’un problème linéaire en nombre entier revient a coder chaque bit des entiers par une variable différente et a déjà été étudié [1]. On pourra s’appuyer sur le fait que les problèmes pour la parallélisation ne manipulent que des nombres entiers de faible amplitude (5 bits avec le signe). La résolution de problème de programmation entière pourra se faire avec PipLIB [5] et pour les problèmes SAT, avec Google OR-tool [6].
Le contenu du stage est le suivant:
Comparaison entre SAT et ILP, problèmes linéaire en nombre entiers, codage binaire des nombres.
Informatique fondamentale
Sid.Touati@inria.fr Sid TOUATI, professeur des universités, Université Côte d’Azur
INRIA Sophia-Antipolis ou Huawei Paris Research (à discuter)
[1] Ruirning Li, Dian Zhou and Donglei Du, ”Satisfiability and integer programming as complementary tools,” ASP-DAC 2004 : Asia and South Pacific Design Automation Conference 2004 (IEEE Cat. No.04EX753), Yokohama, Japan, 2004, pp. 880-883. [2] R. Upadrasta and A. Cohen. 2013. Sub-polyhedral scheduling using (unit-)two- variable-per-inequality polyhedra. SIGPLAN Not. 48, 1 (January 2013), 483–496. [3] Aravind Acharya, Uday Bondhugula, and Albert Cohen. 2018. Polyhedral auto- transformation with no integer linear programming. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2018). [4] B. Pradelle, B. Meister, M. Baskaran, A. Konstantinidis, T. Henretty and R. Le- thin, ”Scalable Hierarchical Polyhedral Compilation,” 2016 45th International Conference on Parallel Processing (ICPP), Philadelphia, PA, USA, 2016, pp. 432-441, doi : 10.1109/ICPP.2016.56. [5] Piplib, http ://www.piplib.org/ [6] SAT Solver, https ://developers.google.com/optimization/reference/sat/sat solver/SatSolver/ [7] Zhao et al, AKG : Automatic Kernel Generation for Neural Processing Units using Polyhedral Transformations, PLDI 2021