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.

Software

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

CO

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

dD

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

DS

Un solveur SAT distribué de solveurs de type 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
  • MIT

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

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

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

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.

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.