Logiciels

Le laboratoire essaye dans la mesure du possible de rendre disponibles les logiciels qu’il produit sous la forme de logiciels libres. Ces logiciels sont identifiés par un badge qui mentionne leur licence libre.

L’usage d’une licence libre a pour but de faciliter la diffusion des résultats de nos recherches dans le monde académique et plus généralement dans notre société numérique. C’est aussi un moyen pour le laboratoire de partager l’effort de maintenance des outils et bibliothèques qu’il conçoit pour ses besoins internes. Ces logiciel sont souvent disponibles « en développement ouvert », sur le compte github du laboratoire ou une autre plateforme de développement collaboratif.

Software

ACE est un solveur de contrainte open-source développé par Christophe Lecoutre (CRIL) en Java.

BE

B+E est un préprocesseur qui associe à une formule CNF d'entrée une formule CNF de sortie qui admet le même nombre de modèles.

bn

bn2cnf est un traducteur associant à un modèle graphique d'entrée (un réseau bayésien ou un réseau de Markov) une sortie qui consiste en une formule CNF et une carte de poids.

Co

Le compilateur br2cnf est un programme permettant de compiler une instance de révision de croyance CNF donnée en une formule CNF équivalente

Co

cnf2eadt est un compilateur associant à une formule CNF d'entrée une représentation équivalente du langage EADT d'arbres de décision affines.

Co

bm2cnf est un compilateur permettant de transformer une instance de fusion CNF donnée en une formule CNF équivalente.

Co

cn2mddg est un compilateur associant à un réseau de contraintes à domaine fini représenté dans le format XCSP 2.1 une représentation équivalente du langage MDDG de graphes de décision décomposables multivalués.

CO

Le but du projet COSCINUS est d'extraire et de visualiser les habitudes de publications à partir de DBLP.

Software

Un solveur rapide pour l'argumentation abstraite basé sur les contraintes

Software

Un outil d'agrégation de croyances.

Cr

Crusti_g2io est un générateur de graphe basé sur un motif interne/externe.

dD

d-DNNF-reasoner est un outil de raisonnement sur les représentations d-DNNF.

DS

D-Syrup est un solveur SAT distribué original basé sur le paradigme portfolio

Software

d4 est un compilateur de CNF vers d-DNNF pour le comptage de modèles.

Ge

tt2bm est un programme qui peut être utilisé à la fois pour générer des instances d'horaires et pour les transformer en instances de fusion basées sur la distance.

Software

Le prouveur qui élimine agressivement les clauses apprises

Software

Gophersat est une bibliothèque en langage go pour résoudre des problèmes SAT, MaxSAT et pseudo-booléens.

Je

Les jeux de révision des croyances (BRG) s'intéressent à la dynamique des croyances d'un groupe d'agents communicants.

Ji

Une bibliothèque Java de gestion des arguments de la ligne de commande compatible Java 9+

Le

Le SAT Game est une présentation amusante et pédagogique du problème de satisfiabilité (SAT). Essayez de résoudre à la main des instances SAT simples !

Software

Un outil d'analyse de données expérimentales en python

Mi

Il s'agit d'un outil qui utilise l'exploration d'items pour compresser les formules booléennes CNF en utilisant l'encodage de tseitin.

NA

The main purpose of this solver is to experiment nogood recording (with a clause reasoning engine) in Constraint Programming (CP).

pd

pddl2cnf est un traducteur associant à une instance de planification classique codée en PDDL (Planning Domain Definition Language) et à un horizon donné une sortie qui consiste en une formule CNF.

pF

pFactory est une bibliothèque C++ qui simplifie la conception de solveurs multithreads.

Pr

pmc est un préprocesseur associant à une formule CNF d'entrée une formule CNF de sortie qui est soit logiquement équivalente à l'entrée, soit n'a que le même nombre de modèles que l'entrée

Software

PyCSP3 est une librairie Python qui permet de développer de manière déclarative des modèles de problèmes combinatoires sous contraintes.

Py

PyXAI est une bibliothèque Python permettant d’apporter des explications de formes diverses à partir de classifieurs issus de techniques d’apprentissage automatique

Ru

Une bibliothèque logicielle pour générer des instances de test via des règles

ru
  • GPL

contrôler finement les ressources mémoire et CPU d'un logiciel lors de son exécution

SA

SAF est un outil de calcul d'attracteurs dans des réseaux de régulation de gênes.

Sa

SATMiner est une bibliothèque pour la recherche de motifs intéressants à l'aide de la programmation par contraintes/SAT.

SA

Pour connaître les dernières nouvelles autour du problème SAT.

Software

SAT4J est une bibliothèque de raisonnement booléen (SAT, MAXSAT, Pseudo-Booléen) en Java.

Sy

Implémente un cadre pour briser les symétries dans les problèmes de fouille d'itemset.

th

Le but du projet OpenCycloDB est de fournir des données ouvertes fiables concernant les cyclodextrines pour faciliter leur usage dans le cadre de l'apprentissage automatique.

To

Il s'agit d'un algorithme pour énumérer les modèles Top-k d'une formule propositionnelle CNF.

Tr

cn2cnf est un traducteur associant à un réseau de contraintes d'entrée (en XCSP3) une formule CNF.

Vi

Etude de la problématique de la planification de parcours de visite de musées, ressources et prototype.

Software

XCSP3 est un format universel, basé sur XML, permettant de représenter des instances de problèmes combinatoires sous contraintes.