January 13, 2020
Yann Strozecki (Laboratoire DAVID )Énumérer des objets est une tâche courante en informatique, que ça soit pour les compter, trouver une solution optimale ou constituer une librairie d’objets intéressants. Un problème typique est de devoir gérer la répétition d’objets identiques (donc inutiles) lors du processus d’énumération. La seule difficulté dans l’énumération des modèles d’une formule DNF est de cette nature. Cela a pour conséquence que les algorithmes habituels utilisent un temps linéaire en la taille de la formule par modèle. Les modèles pouvant être exponentiellement plus petit que la formule, on voudrait donc obtenir un temps linéaire (ou polynomial) en chaque modèle. Nous conjecturons que de tels algorithmes n’existent pas. Néanmoins nous allons montrer comment on peut relâcher le problème ou restreindre les entrées et ainsi proposer plusieurs techniques pour générer ces modèles en temps sous linéaire (par solution générée) voire en temps constant.