Romain Wallon, Maître de Conférences à l’Université d’Artois Romain Wallon

We consider bounded width CNF-formulas where the width is measured by popular graph width measures on graphs associated to CNF-formulas. Such restricted graph classes, in particular those of bounded treewidth, have been extensively studied for their uses in the design of algorithms for various computational problems on CNF-formulas. Here we consider the expressivity of these formulas in the model of clausal encodings with auxiliary variables. We first show that bounding the width for many of the measures from the literature leads to a dramatic loss of expressivity, restricting the formulas to such of low communication complexity. We then show that the width of optimal encodings with respect to different measures is strongly linked: there are two classes of width measures, one containing primal treewidth and the other incidence cliquewidth, such that in each class the width of optimal encodings only differs by constant factors. Moreover, between the two classes the width differs at most by a factor logarithmic in the number of variables. Both these results are in stark contrast to the setting without auxiliary variables where all width measures we consider here differ by more than constant factors and in many cases even by linear factors.

Current implementations of pseudo-Boolean (PB) solvers working on native PB constraints are based on the CDCL architecture which empowers highly efficient modern SAT solvers. In particular, such PB solvers not only implement a (cutting-planes-based) conflict analysis procedure, but also complementary strategies for components that are crucial for the efficiency of CDCL, namely branching heuristics, learned constraint deletion and restarts. However, these strategies are mostly reused by PB solvers without considering the particular form of the PB constraints they deal with. In this paper, we present and evaluate different ways of adapting CDCL strategies to take the specificities of PB constraints into account while preserving the behavior they have in the clausal setting. We implemented these strategies in two different solvers, namely Sat4j (for which we consider three configurations) and RoundingSat. Our experiments show that these dedicated strategies allow to improve, sometimes significantly, the performance of these solvers, both on decision and optimization problems.

Current pseudo-Boolean solvers implement different variants of the cutting planes proof system to infer new constraints during conflict analysis. One of these variants is generalized resolution, which allows to infer strong constraints, but suffers from the growth of coefficients it generates while combining pseudo-Boolean constraints. Another variant consists in using weakening and division, which is more efficient in practice but may infer weaker constraints. In both cases, weakening is mandatory to derive conflicting constraints. However, its impact on the performance of pseudo-Boolean solvers has not been assessed so far. In this paper, new application strategies for this rule are studied, aiming to infer strong constraints with small coefficients. We implemented them in Sat4j and observed that each of them improves the runtime of the solver. While none of them performs better than the others on all benchmarks, applying weakening on the conflict side has surprising good performance, whereas applying partial weakening and division on both the conflict and the reason sides provides the best results overall.

Learning pseudo-Boolean (PB) constraints in PB solvers exploiting cutting planes based inference is not as well understood as clause learning in conflict-driven clause learning solvers. In this paper, we show that PB constraints derived using cutting planes may contain irrelevant literals, i.e., literals whose assigned values (whatever they are) never change the truth value of the constraint. Such literals may lead to infer constraints that are weaker than they should be, impacting the size of the proof built by the solver, and thus also affecting its performance. This suggests that current implementations of PB solvers based on cutting planes should be reconsidered to prevent the generation of irrelevant literals. Indeed, detecting and removing irrelevant literals is too expensive in practice to be considered as an option (the associated problem is NP-hard).

We consider bounded width CNF-formulas where the width is measured by popular graph width measures on graphs associated to CNF-formulas. Such restricted graph classes, in particular those of bounded treewidth, have been extensively studied for their uses in the design of algorithms for various computational problems on CNF-formulas. Here we consider the expressivity of these formulas in the model of clausal encodings with auxiliary variables. We first show that bounding the width for many of the measures from the literature leads to a dramatic loss of expressivity, restricting the formulas to such of low communication complexity. We then show that the width of optimal encodings with respect to different measures is strongly linked: there are two classes of width measures, one containing primal treewidth and the other incidence cliquewidth, such that in each class the width of optimal encodings only differs by constant factors. Moreover, between the two classes the width differs at most by a factor logarithmic in the number of variables. Both these results are in stark contrast to the setting without auxiliary variables where all width measures we consider here differ by more than constant factors and in many cases even by linear factors.

We study pseudo-Boolean constraints (PBC) and their special case cardinality constraints (CARD) from the perspective of knowledge representation. To this end, the succinctness of PBC and CARD is compared to that of many standard propositional languages. Moreover, we determine which queries and transformations are feasible in polynomial time when knowledge is represented by PBC or CARD, and which are not (unconditionally or unless P = NP). In particular, the advantages and disadvantages compared to CNF are discussed.

Les solveurs pseudo-booléens (PB) travaillant nativement sur des contraintes PB sont fondés sur l’architecture CDCL à l’origine des hautes performances des solveurs SAT modernes. En particulier, ces solveurs PB utilisent non seulement une procédure d’analyse de conflits (utilisant les plans-coupes), mais également des stratégies complémentaires qui sont cruciales pour l’efficacité du solveur, comme les heuristiques de choix de variable, de suppression des contraintes apprises et de redémarrage. Cependant, ces stratégies sont le plus souvent réutilisées par les solveurs PB sans tenir compte de la forme particulière des contraintes PB qu’ils considèrent. Dans cet article, nous présentons et évaluons différentes manières d’adapter ces stratégies pour tenir compte des spécificités des contraintes PB tout en préservant le même comportement que dans le cadre clausal. Nous avons implanté ces stratégies dans deux solveurs différents, à savoir Sat4j (pour lequel nous considérons trois configurations) et RoundingSat. Nos expérimentations montrent que ces stratégies dédiées permettent d’améliorer, parfois significativement, les performances de ces solveurs, à la fois sur des problèmes de décision et d’optimisation.

Le développement de solveurs de contraintes s’accompagne nécessairement d’une phase d’expérimentation, permettant d’évaluer les performances des fonctionnalités implantées. Pour chacun des solveurs considérés, il faut alors collecter et analyser des statistisques relatives à leur exécution et qui, le plus souvent, restent les mêmes. Néanmoins, il existe probablement autant de scripts permettant d’extraire ces statistiques et de tracer les figures associées que de chercheurs du domaine. Un outil unifiant et facilitant les analyses de résultats expérimentaux paraît donc nécessaire, notamment pour favoriser le partage et la reproductibilité de ces résultats. Partant de ce constat, nous avons développé la bibliothèque Metrics, dont l’ambition est de fournir une chaîne complète d’outils conçue dans cette optique. Dans cet article, nous présentons cette bibliothèque et illustrons son utilisation en rejouant l’analyse des résultats de la compétition XCSP’19.

L’apprentissage de contraintes pseudo-booléennes (PB) dans les solveurs PB via le système de preuve des plans-coupes n’est pas aussi bien compris que celui des clauses dans les solveurs SAT utilisant l’analyse de conflit. En particulier, les approches basées sur la résolution généralisée peuvent déduire des contraintes PB comportant des littéraux non pertinents, i.e., des littéraux dont la valeur de vérité (quelle qu’elle soit) ne change jamais la valeur de vérité de la contrainte. Cela peut se produire même quand la formule PB considérée en entrée ne comporte pas de tels littéraux. Nous observons expérimentalement de telles situations sur des instances de l’évaluation pseudo-booléenne 2016. Nous montrons que la détection des littéraux non pertinents dans les contraintes PB apprises, bien que calculatoirement difficile, peut avoir un impact positif sur le temps d’exécution des solveurs (dans notre cas, Sat4j), en permettant le retrait de ces littéraux.

Current PB solvers implement many techniques inspired by the CDCL architecture of modern SAT solvers, so as to benefit from its practical efficiency. However, they also need to deal with the fact that many of the properties leveraged by this architecture are no longer true when considering PB constraints. In this paper, we focus on one of these properties, namely the optimality of the so-called first unique implication point (1-UIP). While it is well known that learning the first assertive clause produced during conflict analysis ensures to perform the highest possible backjump in a SAT solver, we show that there is no such guarantee in the presence of PB constraints. We also introduce and evaluate different approaches designed to improve the backjump level identified during conflict analysis by allowing to continue the analysis after reaching the 1-UIP. Our experiments show that sub-optimal backjumps are fairly common in PB solvers, even though their impact on the solver is not clear.

Current implementations of pseudo-Boolean (PB) solvers are based on the CDCL architecture, which is the central component of modern SAT solvers. In addition to clause learning, this architecture comes with many strategies that help the solver find its way through the search space, either to a solution or to an unsatisfiability proof. Particularly important are the decision heuristic, but also other features like learned clause deletion or restarts. Currently, these strategies are mostly used “as is” in PB solvers, without considering the particular form of the PB constraints they deal with. In this paper, we introduce new ways of adapting these strategies to better take into account the specificities of such constraints, especially regarding their weights and propagation properties. In particular, our experiments show that carefully considering these criteria may have a significant impact on the performance of the solver.

When developing a SAT solver, one of the most important parts is to perform experiments so as to evaluate its performance. Most of the time, this process remains the same, so that everybody collects almost the same statistics about the solver execution. However, how many scripts are there to retrieve experimental data and draw scatter or cactus plots? Probably as many as researchers in the domain. Based on this observation, this paper introduces Metrics, a Python library, aiming to unify and make easier the analysis of solver experiments. The ambition of Metrics is to provide a complete toolchain from the execution of the solver to the analysis of its performance. In particular, this library simplifies the retrieval of experimental data from many different inputs (including the solver’s output), and provides a nice interface for drawing commonly used plots, computing statistics about the execution of the solver, and effortlessly organizing them (e.g., in Jupyter notebooks). In the end, the main purpose of Metrics is to favor the sharing and reproducibility of experimental results and their analysis.

Learning pseudo-Boolean (PB) constraints in PB solvers using the cutting planes proof system is a problem that is not as well understood as clause learning in conflict driven clause learning solvers. In particular, it turns out that approaches based on generalized resolution may derive PB constraints containing irrelevant literals, i.e., literals whose assigned values (whatever they are) never change the truth value of the constraint. This may happen even when starting from inputs without irrelevant literals. We observe such situations empirically on benchmarks from the latest PB evaluation. We perform an experiment exhibiting the negative impact of irrelevant literals on the runtime of solvers, by showing that their removal may be beneficial, in our case to Sat4j.

Cette thèse porte sur le langage des conjonctions de contraintes pseudo-booléennes, formées d’équations ou inéquations linéaires en variables booléennes. Ce format généralise le format CNF très répandu. Notre contribution à l’étude des contraintes pseudo-booléennes se compose de deux parties.

Dans une première partie, nous étudions les contraintes pseudo-booléennes du point de vue de la représentation des connaissances. Nous comparons leur langage à différents formats propositionnels largement utilisés en évaluant chacun d’eux à l’aune des critères de la carte de compilation proposée par Darwiche et Marquis. Cette comparaison montre, d’un côté, l’un des avantages des contraintes pseudo-booléennes par rapport aux formules CNF : elles peuvent être beaucoup plus concises. Malheureusement, d’un autre côté, les opérations qui sont NP-difficiles pour les contraintes pseudo-booléennes sont plus nombreuses que pour les formules CNF. En conséquence, il est parfois préférable d’utiliser des encodages CNF (au lieu d’utiliser des représentations) de ces contraintes. De cette manière, l’efficacité en pratique des solveurs SAT modernes peut être mise à profit pour raisonner sur de tels encodages. Nous étudions également les propriétés de ces encodages, et montrons que borner leur largeur peut fortement réduire leur expressivité.

L’une des raisons pour lesquelles il est intéressant d’utiliser des contraintes pseudo-booléennes en plus des formules CNF est qu’elles permettent d’utiliser le système de preuve des plans coupes, qui est plus puissant que celui de la résolution implanté dans les solveurs SAT classiques pour raisonner sur des formules CNF. En particulier, des preuves d’incohérence produites par ce système de preuve peuvent être exponentiellement plus courtes que leur équivalent dans le système de la résolution pour certains ensembles de contraintes. Ainsi, d’un point de vue théorique, les solveurs pseudo-booléens, capables de prendre en compte nativement les contraintes pseudo-booléennes, pourraient être plus efficaces que les solveurs SAT. Cependant, en pratique, les solveurs pseudo-booléens ne tiennent pas cette promesse, et il est important de comprendre pourquoi.

Comme une étape dans cette direction, la deuxième partie de cette thèse est consacrée à la résolution pratique de problèmes pseudo-booléens. Nous identifions plusieurs faiblesses des solveurs pseudo-booléens, et proposons des améliorations. En particulier, nous montrons que toutes les règles implantées par les solveurs pseudo-booléens peuvent produire, pendant l’analyse de conflit, des littéraux non pertinents, c’est-à-dire des littéraux dont la valeur de vérité n’influe pas sur celle des contraintes dans lesquelles ils apparaissent. Ce comportement est problématique, puisque ces littéraux conduisent à l’inférence de contraintes plus faibles, et donc à la production de preuves d’incohérence plus longues. Nous proposons plusieurs approches pour corriger ces faiblesses, comme l’utilisation de nouvelles stratégies d’affaiblissement, visant à établir un compromis entre la taille des contraintes produites et leur force. Ces stratégies peuvent permettre d’éliminer efficacement des littéraux non pertinents, même si elles produisent des contraintes plus faibles. Nous montrons par ailleurs qu’un affaiblissement plus parcimonieux (mais inévitable) peut permettre d’améliorer les performances du solveur.

De plus, nous adaptons au cadre pseudo-booléen un certain nombre de variantes de stratégies implantées par les solveurs SAT classiques. En particulier, nous présentons des heuristiques et des mesures pour la qualité des contraintes apprises dédiées aux contraintes pseudo-booléennes. Nous montrons qu’un choix avisé parmi ces stratégies peut permettre d’améliorer considérablement les performances du solveur.

Toutes les approches pratiques décrites dans cette thèse ont été implantées dans le solveur pseudo-booléen Sat4j et sont publiquement accessibles.

Le problème de la cohérence propositionnelle est le problème NP-complet de référence, qui se retrouve dans de nombreuses applications de la vie de tous les jours. Même si de récentes avancées dans ce domaine ont permis d’améliorer l’efficacité des solveurs, certaines instances de ce problème ne peuvent être résolues en un temps raisonnable. Lorsque des garanties de temps de réponse sont attendues, il n’est dès lors pas possible d’utiliser ces solveurs en l’état. Il faut donc considérer différentes approches.

Une première idée est de considérer un langage différent pour modéliser nos problèmes, par exemple celui des contraintes pseudo-booléennes. En les associant au système de preuve des plans-coupes, nous disposons d’un système plus puissant que celui de la résolution, traditionnellement utilisé par les solveurs SAT. À titre d’exemple, le problème des pigeons peut être résolu en temps linéaire avec cette approche, contre un temps exponentiel pour l’approche par résolution.

Afin d’améliorer la résolution pratique d’instances du problème SAT partageant une partie commune, une autre approche consiste à compiler cette partie commune sous une forme compacte, sur laquelle effectuer des requêtes est calculatoirement plus facile. Dans ce rapport, nous nous intéressons également à l’utilisation des contraintes pseudo-booléennes dans ce contexte.

Le problème de satisfaisabilité d’une formule propositionnelle en forme normale conjonctive (SAT) est un problème complexe qui intervient dans la vie de tous les jours, qu’il s’agisse de planifier des tâches, de configurer les options de sa voiture ou encore de jouer au Sudoku. Le problème du comptage de modèles d’une formule propositionnelle en forme normale conjonctive (#SAT), qui est encore plus difficile du point de vue de la complexité algorithmique, trouve lui aussi de nombreuses applications, par exemple pour le calcul d’inférence probabiliste ou la planification dans l’incertain.

Le théorème de Toda affirme que, si l’on est capable de compter efficacement les modèles de toute formule CNF – typiquement, en considérant l’utilisation d’un oracle, il est possible de résoudre efficacement l’ensemble des problèmes de la hiérarchie polynomiale. Ceci souligne à la fois l’importance de #SAT, mais aussi sa complexité.

Afin d’améliorer la résolution pratique d’instances de #SAT partageant une partie commune, il peut être utile de passer par une phase de compilation : il s’agit de représenter cette partie commune sous une forme compacte et facilement interprétable par la machine. Une fois la compilation effectuée, certaines requêtes, dont le comptage de modèles, sont faciles (à partir de la représentation compilée obtenue).

Pour faciliter le comptage de ses modèles ou sa compilation sous forme de circuits du langage d-DNNF (les représentations sous forme normale négative décomposable et déterministe), il est intéressant de décomposer l’instance CNF considérée. Il existe pour cela plusieurs algorithmes, comme la tree-decomposition ou la décomposition en dtrees, qui, à partir d’un graphe associé à l’instance considérée, permettent d’obtenir un arbre, calculatoirement plus simple à exploiter. Les arbres ainsi obtenus ont une complexité mesurée par leur largeur, appelée treewidth. Celle-ci joue un rôle majeur, à la fois dans la compilation sous forme d-DNNF et dans le comptage de modèles, puisque, ces opérations s’effectuent en 𝒪(n.2^treewidth). Autrement dit, lorsque la treewidth est bornée, elles s’effectuent en temps linéaire.

Le calcul exact de la treewidth d’un graphe étant difficile, il importe de définir de bonnes heuristiques pour calculer des décompositions ayant une treewidth raisonnable.