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.

Logiciels pérennes

Ces logiciels sont écrits et maintenus durablement par des membres permanents du laboratoire.

  • AbsCon
    AbsCon permet de résoudre des problèmes combinatoires sous contraintes (CSP, COP, WCSP).
  • COSCINUS, Statistiques de publications en informatique
    Le but du projet COSCINUS est d'extraire et de visualiser les habitudes de publications à partir de DBLP.
  • Glucose MIT
    Le prouveur qui élimine agressivement les clauses apprises
  • SAT4J EPLLGPL
    SAT4J est une bibliothèque de raisonnement booléen (SAT, MAXSAT, Pseudo-Booléen) en Java.
  • XCSP
    XCSP3 is a XML-based format designed to represent combinatorial constrained problems.
  • runsolver GPL
    contrôler finement les ressources mémoire et CPU d'un logiciel

Logiciels récents

  • CoQuiAAS GPL
    Un solveur rapide pour l'argumentation abstraite basé sur les contraintes
  • Gophersat MIT
    Gophersat est une bibliothèque en langage go pour résoudre des problèmes SAT, MaxSAT et pseudo-booléens.
  • Jigsaw-CLI GPL
    Une bibliothèque Java de gestion des arguments de la ligne de commande compatible Java 9+
  • NACRE GPL
    The main purpose of this solver is to experiment nogood recording (with a clause reasoning engine) in Constraint Programming (CP).
  • Rubens GPL
    Une bibliothèque logicielle pour générer des instances de test via des règles
  • d4
    d4 est un compilateur de CNF vers d-DNNF pour le comptage de modèles.
  • mETRICS - rEproducible sofTware peRformance analysIs in perfeCt Simplicity LGPL
    Un outil d'analyse de données expérimentales en python
  • pFactory, a library for multithreaded SAT solvers GPL
    pFactory is a C++ library that simplifies the design of multithreaded solvers.

Prouveurs CSP & SAT

  • AbsCon
    AbsCon permet de résoudre des problèmes combinatoires sous contraintes (CSP, COP, WCSP).
  • AmPharoS
    Un solveur SAT distribué basé sur le paradigme diviser pour régner
  • D-Syrup
    Un solveur SAT distribué de solveurs de type portfolio
  • Glucose MIT
    Le prouveur qui élimine agressivement les clauses apprises
  • Gophersat MIT
    Gophersat est une bibliothèque en langage go pour résoudre des problèmes SAT, MaxSAT et pseudo-booléens.
  • ManySat
    ManySat est un solveur parallèle de type DPLL incluant toute les fonctionnalités des solveurs SAT modernes (analyse de conflits, heuristique basée sur les activités, etc.) et celles issues de nos résultats récents sur l’amélioration des techniques d’analyse de conflits.
  • NACRE GPL
    The main purpose of this solver is to experiment nogood recording (with a clause reasoning engine) in Constraint Programming (CP).
  • Penelope
    La résolution parallèle de SAT basée sur le LBD et le PSM.
  • ReViVal
    ReViVal est une technique de simplification (ou de vivification) de formules CNF.
  • SAT4J EPLLGPL
    SAT4J est une bibliothèque de raisonnement booléen (SAT, MAXSAT, Pseudo-Booléen) en Java.
  • pFactory, a library for multithreaded SAT solvers GPL
    pFactory is a C++ library that simplifies the design of multithreaded solvers.
  • ppfolio GPL
    Le solveur SAT aux 16 médailles à la compétition SAT de 2011

Raisonnement

  • Belief Revision Games
    Belief revision games (BRGs) are concerned with the dynamics of the beliefs of a group of communicating agents.
  • CoQuiAAS GPL
    Un solveur rapide pour l'argumentation abstraite basé sur les contraintes
  • PRISM GPL
    PRISM stands for Platform for Reasoning with Inconsistency Shapley Measure.

Compilateurs

  • Le projet Compile!
    Le projet Compile! rassemble les travaux réalisés au CRIL sur le thème de la compilation de connaissances.
  • d4
    d4 est un compilateur de CNF vers d-DNNF pour le comptage de modèles.

Fouille de données déclarative

  • DecMining
    DecMining is a web page dedicated to declarative approaches for data mining. It contains software, datasets, publications and related links to others research groups.

Solveur de jeu

  • Woodstock
    Woodstock est un solveur de jeux pour le General Game Playing basé sur les CSP stochastiques.

Autres

Sites web

  • COSCINUS, Statistiques de publications en informatique
    Le but du projet COSCINUS est d'extraire et de visualiser les habitudes de publications à partir de DBLP.
  • Le SAT Game
    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 !
  • SAT Live!
    Pour connaître les dernières nouvelles autour du problème SAT.
  • XCSP
    XCSP3 is a XML-based format designed to represent combinatorial constrained problems.

Anciens logiciels développés au CRIL