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.

Abstract

Model counting and sampling are two fundamental problems in artificial intelligence. The theory of these problems goes back to the 1980s. There are different problems in various areas like machine learning, planning, statistics and so on which are known to be computationally hard. Even finding a single solution can be a struggle for such problems; counting the number of solutions is much harder. Thus, approximate model counting could be useful to solve them. The idea of this work comes from previous works which are focused more on binary variables. They use hashing-based techniques by generating random XOR constraints to partition the solution space into small cells and then use a SAT solver to count inside a random cell. SAT solvers are used for binary domains but we propose here to use CP solvers for non-binary domains. The goal of this research is to present an algorithm for approximately counting the number of solutions of a CP model. In the first step, we start to divide the solution space into p small cells at each added mod p constraint according to modular arithmetic p. Then by using the Gauss-Jordan elimination algorithm we try to simplify the system of randomly generated linear constraints. Moreover we introduce an algorithm that by creating a graph incrementally filters variable domains in one random small cell. After counting the number of solutions in one small cell we estimate the number of solutions by multiplying the number of solutions in one cell by the number of cells.