International Journal on Artificial Intelligence Tools

The set of novelties introduced with the SAT solver Glucose is now considered as a standard for practical SAT solving. In this paper, we review the different strategies and technologies added in Glucose over the years. We detail each technique and discuss its impact on the final performances reached by Glucose. We also come back on one of the main developments of the solver over the very last years: its efficient parallelization. We extensively tested different versions of Glucose and Syrup (its parallel version) on all the benchmarks since 2011. By including, as a reference, the SAT solver Lingeling (and its parallel version Plingeling), we show that Glucose and Syrup are significantly faster than other solvers, even if they can solve fewer instances.

Several propositional satisfiability (SAT) based encodings have been proposed to deal with various data mining problems including itemset and sequence mining problems. This research issue allows to model data mining problems in a declarative way, while exploiting efficient SAT solving techniques. In this paper, we overview our contributions on the application of propositional satisfiability (SAT) to model and solve itemset mining tasks. We first present a SAT based encoding of frequent closed itemset mining task as a propositional formula whose models corresponds to the patterns to be mined. Secondly, we show that some data mining constraints can be avoided by reformulation. We illustrate this issue by reformulating the closeness constraint using the notion of minimal models. Finally, we also addressed the scalability issue, one of the most important challenge of these nice declarative framework. To this end, we proposed a complete partition based approach whose aim is to avoid encoding the whole database as a single formula. Using a partition on the set of items, our new approach leads to several propositional formulas of reasonable size. The experimental evaluation on several known datasets shows huge improvements in comparison to the direct approach without partitioning, while reducing significantly the performance gap with respect to specialized algorithms.

In June 2008, the Eclipse open platform released a new dependency management system called p2. That system was based on the translation of the dependency management problem into a pseudo-Boolean optimization problem, to be handled by the Sat4j solver. Since then, p2 has been more tightly integrated with Sat4j, the platform opened a public plugin repository (the Eclipse marketplace) which relies on p2 to install the available plugins and their dependencies, and became the favorite way to install plugins in the Eclipse community. This paper summarizes the issues raised by Eclipse dependency management, its pseudo-Boolean encoding within p2, its extension for Linux package management with p2cudf, and concludes with lessons learned on using research software in production systems.

Consensus-finding is a ubiquitous paradigm in both A.I. and everyday life. Recently, a computational approach to consensus-finding has been introduced in the standard clausal Boolean logic framework. It captures non-contradictory fragments of the information conveyed by different agents such that these fragments do not logically conflict with any of the agents. This kind of consensuses concerns open-minded agents: On one side, these agents accept to drop their own information that contradicts other agents. On the other side, they can accept any information from another agent provided that this latter information does not contradict them. In this study, it is shown that a family of consensuses might not actually be endorsed by these open-minded agents, due to the usual ad-hoc logical representation of knowledge and well-known paradoxes linked to material implication. Accordingly, we trim the set of consensuses by filtering out these undesirable consensuses and keep so-called admissible consensuses, only. A computational approach that is based on the SAT technologies and that delivers one maximal admissible consensus is then investigated.