Romain Wallon, Associate Professor at Artois University 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.

This thesis is about the language of pseudo-Boolean constraints, i.e., of conjunctions of linear equations or inequations over Boolean variables, that generalizes the well-known CNF format. Our contribution to the study of this language is twofold.

In the first part of the thesis, the language of pseudo-Boolean constraints is investigated from a knowledge representation perspective. It is compared to a number of well-known propositional formats using the criteria considered in the so-called knowledge compilation map pointed out by Darwiche and Marquis. On the one hand, an advantage of using pseudo-Boolean constraints as a representation language over CNF formulae is that they can be far more succinct. On the other hand, unfortunately, more operations of interest are NP-hard when dealing with pseudo-Boolean constraints compared to CNF formulae. As a consequence, it is sometimes preferable to consider CNF encodings (instead of CNF representations) of such constraints. Doing so, the practical efficiency of modern SAT solvers can be leveraged to reason with these encodings. We also investigate the properties of such encodings, and show that bounding their width may drastically reduce their expressivity.

One reason for considering pseudo-Boolean constraints instead of CNF formulae is that they allow the use of the cutting planes proof system, which is stronger than the resolution proof system implemented in classical SAT solvers based on CNF. In particular, unsatisfiability proofs that may be exponentially shorter than their resolution counterpart can be derived for some sets of pseudo-Boolean constraints. Thus, from the theory side, pseudo-Boolean solvers, i.e., solvers that use pseudo-Boolean constraints natively instead of encodings, could be more efficient than SAT solvers. However, practical solver implementations fail to keep this promise, and understanding why this is the case is an important issue.

As a step in this direction, the second part of this thesis deals with the practical resolution of pseudo-Boolean problems. Several weaknesses of current implementations of pseudo-Boolean solvers are identified and for some of them improvements are proposed. In particular, we show that all rules implemented in pseudo-Boolean solvers may produce irrelevant literals during conflict analysis, i.e., literals that have no effect on the truth value of the constraints in which they appear. This is problematic as such literals lead to the inference of constraints that can be weaker than expected, and in turn to the production of longer unsatisfiability proofs. We point out several approaches to deal with those weak points, such as the use of new weakening strategies, that are designed in such a way that a tradeoff between the size of the derived constraints and their strength is obtained. Those weakening strategies may allow to efficiently eliminate irrelevant literals, at the price of deriving weaker constraints. In addition, we show that a more parsimonious (but inevitable) application of the weakening rule may allow improving the performance of the solver.

We also lift many variants of strategies that are classically implemented in SAT solvers to the pseudo-Boolean setting. In particular, branching heuristics and quality measures for learned constraints that are adapted to pseudo-Boolean constraints are presented. We show that a careful choice among those strategies may drastically improve the performance of the solver.

All practical approaches described in this thesis have been implemented in the pseudo-Boolean solver Sat4j and are publicly available.

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.