Solving Systems of Linear Equalities in Modular Arithmetic with Applications to Model Counting in Constraint Programming

Le comptage et l'échantillonnage de modèles sont deux problèmes fondamentaux en intelligence artificielle. La théorie de ces problèmes remonte aux années 1980. Il existe différents problèmes dans divers domaines, tels que l'apprentissage automatique, la planification, les statistiques, etc., dont on sait qu'ils sont difficiles à calculer. Même trouver une solution unique peut être une lutte pour de tels problèmes; compter le nombre de solutions est beaucoup plus difficile. Ainsi, le comptage approximatif des modèles pourrait être utile pour les résoudre. L'ideé de ce travail vient des travaux précédents qui sont davantage axés sur les variables binaires. Ils utilisent des techniques basées sur le hachage en générant des contraintes XOR de manière aléatoire pour partitionner l'espace des solutions en petites cellules, puis en utilisant un solveur SAT pour compter à l'intérieur d'une cellule aléatoire. Les solveurs SAT sont utilisés pour les domaines binaires, mais nous proposons ici d'utiliser des solveurs CP pour les domaines non binaires. Le but de cette recherche est de présenter un algorithme permettant de compter approximativement le nombre de solutions d'un modèle de CP. Dans la première étape, nous commençons à diviser l'espace des solutions en p petites cellules à chaque contrainte de mod p ajoutée conformément à l'arithmétique modulaire p. Ensuite, en utilisant l'algorithme d'élimination de Gauss-Jordan, nous essayons de simplifier le système de contraintes linéaires générées aléatoirement. De plus, nous introduisons un algorithme qui, en créant un graphe, filtre les domaines des variables dans une petite cellule aléatoire. Après avoir compté le nombre de solutions dans une petite cellule, nous estimons le nombre de solutions en multipliant le nombre de solutions dans une cellule par le nombre de cellules.