• CPT
    CPT est un planificateur temporel.
  • LSAT
    LSAT est un solveur SAT basé sur la procédure classique DPLL à laquelle a été ajouté un pré-traitement permettant de récupérer et d’exploiter les informations structurelles cachées par la forme normale conjonctive.
  • OpenQBF
    OpenQBF est un prouveur QBF en Java simple mais correct. Il n’est plus maintenu depuis 2004. Le code source du prouveur est disponible sur sourceforge.
  • QBFL
    QBFL est un prouveur QBF prenant avantage des classes polynomiales de ce problème.
  • ValCSP
    valCSP est un solveur de réseaux de contraintes (formalisme CSP). Il s’intéresse aux problèmes de décision liés aux CSP.
  • YAHSP
    YAHSP est un planificateur par recherche heuristique pour la planification classique sous horizon borné.