Missions

La compilation de connaissances est un domaine de recherche qui s'intéresse à des structures de données permettant une représentation succincte des bases de connaissances tout en permettant de raisonner efficacement sur les conséquences logiques de la base de connaissances. En pratique, les bases de connaissances sont interprétés comme des fonctions Booléennes dont les modèles coincident avec les modèles de la base de connaissances. Les structures de données les plus utiles en compilation de connaissances sont donc des structures permettant de représenter succinctement des fonctions Booléennes tout en permettant d'obtenir efficacement des informations sur leurs modèles, comme par exemple en les énumérant, les comptant etc.

Le logiciel d4, développé au CRIL par Jean-Marie Lagniez, permet de construire efficacement ce genre de structure de données. Son architecture reposant sur les SAT solvers en font un des outils les plus efficaces dans ce domaine, en particulier, pour résoudre des problèmes où trouver le nombre de modèles d'une fonction Booléenne est important. Cependant, pour utiliser d4, un utilisateur doit nécessairement l'invoquer depuis la ligne de commande, avec de nombreuses options qui demandent une bonne compréhension des outils théoriques sous-jacents.

La mission principale de la personne recrutée sera de proposer un wrapper Python pour pouvoir utiliser d4 directement depuis Python. Le but sera de réfléchir à une interface simplifiée permettant aux utilisateurs de facilement appréhender d4 pour résoudre des problèmes très concret (comme du comptage). À plus long terme, le but serait d'offrir une interface unifiée permettant d'utiliser différents compilateurs de connaissances sans changer d'interface, un peu comme cela a déjà été fait pour les SAT Solvers avec la librairie PySAT ou les solvers linéaires avec la libraire PULP.

Activités

- Développement d'un wrapper python pour d4
- Élaboration d'une API pour interfacer les compilateurs de connaissances avec Python
- Développement d'un wrapper autour d'un raisonneur écrit en Rust.

Compétences

- Bonne compréhension de la logique propositionnelle
- Bonne maîtrise de C++
- Bonne maîtrise de Python

Compétences optionnelles mais désirables :

- Maîtrise de Rust
- Connaissances de SAT solvers.

Contexte de travail

L'activité sera effectuée au sein du Centre de Recherche en Informatique de Lens. Le CRIL est un laboratoire situé à Lens, spécialisé dans différents aspects de l'intelligence artificielle.