In this paper, we introduce novel methods for drawing conclusions from inconsistent information in a highly cautious manner. While standard paraconsistent approaches typically rely on the formulas in the intersection of maximally consistent subsets, known as the free formulas, we argue that not all these formulas share the same degree of reliability. Our refined reasoning frameworks distinguish between free formulas, based on their actual involvement in the inconsistency, an so enabling inference only when conclusions are robustly supported. These methods are particularly valuable in high-stakes contexts where decisions carry irreversible or far-reaching consequences. We present several implementation techniques grounded in multi-valued semantics and syntactic independence, analyze their fundamental logical properties, and establish a hierarchy of their inferential strength.

Inconsistency measures quantify the degree of conflict within a set of propositions. They can be broadly categorized into global measures, which assess the overall inconsistency of a set, and local measures, which evaluate the contribution of single formulas to the overall inconsistency. This paper investigates the relationship between these two classes of measures through the lens of marginal contributions and pooling mechanisms. We propose a systematic framework for deriving local inconsistency measures from global ones by employing notions of marginal contributions inspired by cooperative game theory, including Shapley and Banzhaf values. Conversely, we explore methods for constructing global inconsistency measures by aggregating local contributions using various pooling techniques. A key research question arises: which combinations of marginal contribution notions (maC) and pooling mechanisms (P) are compatible? Compatibility is defined such that, given a global measure I, applying (P) to the marginal contributions derived from I yields the same result as directly applying I, and vice versa. We analyze this compatibility condition and identify specific pairs of methods, (maC) and (P), that satisfy it across various inconsistency frameworks. Our findings provide a deeper understanding of the interplay between global and local inconsistency measures, providing a foundation for designing principled and interpretable inconsistency evaluation methods in logic-based systems.

Conceptual clustering is a well-studied research area in the field of unsupervised machine learning. It aims to identify disjoint clusters, where each cluster represents a collection of similar transactions described by a common pattern. The first phase of earlier conceptual clustering methods relies on the enumeration of closed patterns. Nevertheless, the extraction of such patterns can be challenging, primarily due to their rigorous nature. Indeed, closed patterns can be not frequent or fail to cover all the transactions within a cluster. To overcome this issue, this paper presents a novel approach based on the relaxation of frequent patterns called k-relaxed frequent patterns. Then, we introduce a propositional satisfiability method for enumerating such patterns. Afterwards, we employ an integer linear programming approach to compute the set of disjoint clusters. Finally, we demonstrate the efficiency of our approach through an extensive experiments conducted on several popular real-life datasets.

Explainability is a fundamental principle in the field of Artificial Intelligence (AI), ensuring that AI models and systems are understandable and transparent to end-users. Specifically, it tackles the challenge of providing explanations for AI predictions. In interpretable machine learning, classification rules are regarded one of the most well-known explainability techniques, due to their expressive power and transparent structure. In this paper, we first show that computing classification rules is equivalent to mining disjunctive patterns from the corresponding transaction database. Second, we show that our approach provides a clear characterization of optimal classification rules, wherein disjunctive patterns satisfy the non-redundancy property in the target class and such patterns correspond to minimal generators in this class. Then, we propose a SAT-based solution of the problem for computing optimal classification rules using MaxSAT solvers, for which the optimality is a balancing between the accuracy and the size of the rules. Finally, we present an empirical evaluation on several representative datasets, showing that our approach achieves good performance in terms of accuracy and interpretability compared to existing baselines.

Conflicts are inherent to normative systems. In this paper, we explore a novel approach to normative reasoning by quantifying the amount of conflicts within normative systems. We refine the idea from classical logic, according to which a formula is a consequence of a knowledge base in case its negation renders the knowledge base inconsistent. In our approach, whether a formula is a logical consequence depends, for instance, on its negation's marginal contribution to the inconsistency of the given knowledge base. Accordingly, various inconsistency measures and corresponding (nonmonotonic and paraconsistent) normative entailment relations are analyzed relative to a number of logical properties. To illustrate our approach, we adopt Input/Output logic, a renowned formalism in deontic logic, specifically designed for defeasible normative reasoning. As an application, the resulting entailment relations provide recommendations to agents for minimizing norm conflicts, and may be incorporated in a number of implementations (like the Tweety libraries and the LogiKey framework) by involving inconsistency measurements in normative reasoning.

International audience

In formal argumentation, a distinction can be made between extension-based semantics, where sets of arguments are either (jointly) accepted or not, and ranking-based semantics, where grades of accept- ability are assigned to arguments. Another important distinction is that between abstract approaches, that abstract away from the content of arguments, and structured approaches, that specify a method of constructing argument graphs on the basis of a knowledge base. While ranking-based semantics have been extensively applied to abstract argumentation, few work has been done on ranking-based semantics for structured argumentation. In this paper, we make a systematic investigation into the be- haviour of ranking-based semantics applied to existing formalisms for structured argumentation. We show that a wide class of ranking-based semantics gives rise to so-called culpability measures, and are relatively robust to specific choices in argument construction methods.

The computation of minimal rare itemsets is a well known task in data mining, with numerous applications, e.g., drugs effects analysis and network security, among others. This paper presents a novel approach to the computation of minimal rare itemsets. First, we introduce a generalization of the traditional minimal rare itemset model called k-minimal rare itemset. A k-minimal rare itemset is defined as an itemset that becomes frequent or rare based on the removal of at least k or at most (k − 1) items from it. We claim that our work is the first to propose this generalization in the field of data mining. We then present a SAT-based framework for efficiently discovering k-minimal rare itemsets from large transaction databases. Afterwards, by partitioning the k-minimal rare itemset mining problem into smaller sub-problems, we aim to make it more manageable and easier to solve. Finally, to evaluate the effectiveness and efficiency of our approach, we conduct extensive experimental analysis using various popular datasets. We compare our method with existing specialized algorithms and CP-based algorithms commonly used for this task.

Association rule mining is one of the well-studied and most important knowledge discovery task in data mining. In this paper, we first introduce the k-disjunctive support based itemset, a generalization of the traditional model of itemset by allowing the absence of up to k items in each transaction matching the itemset. Then, to discover more expressive rules from data, we define the concept of (k, k′)-disjunctive support based association rules by considering the antecedent and the consequent of the rule as k-disjunctive and k′-disjunctive support based itemsets, respectively. Second, we provide a polynomial-time reduction of both the problems of mining k-disjunctive support based itemsets and (k, k′)-disjunctive support based association rules to the propositional satisfiability model enumeration task. Finally, we show through an extensive campaign of experiments on several popular real-life datasets the efficiency of our proposed approach

Ranking is ubiquitous in everyday life. This paper is concerned with the problem of ranking information of a knowledge base when this latter is possibly inconsistent. In particular, the key issue is to elicit a plausibility order on the formulas in an inconsistent knowledge base. We show how such ordering can be obtained by using only the inherent structure of the knowledge base. We start by introducing a principled way a reasonable ranking framework for formulas should satisfy. Then, a variety of ordering criteria have been explored to define plausibility order over formulas based on consistency. Finally, we study the behaviour of the different formula ranking semantics in terms of the proposed logical postulates as well as their (in)-compatibility.

Mining interesting patterns from data is a core part of the data mining world. High utility mining, an active research topic in data mining, aims to discover valuable itemsets with high profit (e.g., cost, risk). However, the measure of interest of an itemset must primarily reflect not only the importance of items in terms of profit, but also their occurrence in data in order to make more crucial decisions. Some proposals are then introduced to deal with the problem of computing high utility itemsets that meet a minimum support threshold. However, in these existing proposals, all transactions in which the itemset appears are taken into account, including those in which the itemset has a low profit. So, no additional information about the overall utility of the itemset is taken into account. This paper addresses this issue by introducing a SAT-based model to efficiently find the set of all frequent high utility itemsets with the use of a minimum utility threshold applied to each transaction in which the itemset appears. More specifically, we reduce the problem of mining frequent high utility itemsets to the one of enumerating the models of a formula in propositional logic, and then we use state-of-the-art SAT solvers to solve it. Afterwards, to make our approach more efficient, we provide a decomposition technique that is particularly suitable for deriving smaller and independent sub-problems easy to resolve. Finally, an extensive experimental evaluation on various popular datasets shows that our method is fast and scale well compared to the state-of-the art algorithms.

Computing high utility motifs is a fundamental data mining method for discovering useful itemsets yielding high utility values. Minimal and maximal high utility itemsets are two examples of compact representations used to reduce the output size due to the large and incomprehensible number of patterns. In this paper, we present a novel method for mining minimal and maximal high utility itemsets using propositional satisfiability. First, we show that minimal and maximal high utility patterns are X-minimal models of a CNF formula. Then, to improve the scalability issue of our method, we harness a decomposition paradigm that splits the transaction database into smaller and independent transaction sub-bases, allowing an efficient enumeration of minimal and maximal high utility itemsets. Finally, through extensive evaluation studies on various real-world datasets, we demonstrate that our approach is very competitive w.r.t. to the state-of-the-art specialized solutions.

Gradual itemsets model complex attributes covariations of the form the more or less is A, the more or less is B. Recently, such kind of itemsets has received great attention over the last years, and several proposals have been introduced to automatically extract these patterns from numerical databases. Unfortunately, discovering such itemsets remains challenging because of the exponential combinatorial search space.In this paper, we first formalize the problem of mining gradual itemsets as a constraint-based problem. Then, we use SAT solvers for solving the corresponding propositional satisfiability problem. Extensive experiments on real-world datasets confirm that our proposal is competitive with GRITE, one of the most efficient state-of-the-art algorithm for discovering frequent gradual itemsets. Lastly, we show the flexibility of our SAT-based approach by its ability to modeling additional user constraints without revising the solving process.

While traditional data mining techniques have been used extensively for finding patterns in databases, they are not always suitable for incorporating user-specified constraints. To overcome this issue, CP and SAT based frameworks for modeling and solving pattern mining tasks have gained a considerable audience in recent years. However, a bottleneck for all these CP and SAT-based approaches is the encoding size which makes these algorithms inefficient for large databases. This paper introduces a practical SAT-based approach to discover efficiently (minimal non-redundant) association rules. First, we present a decomposition-based paradigm that splits the original transaction database into smaller and independent subsets. Then, we show that without producing too large formulas, our decomposition method allows independent mining evaluation on a multi-core machine, improving performance. Finally, an experimental evaluation shows that our method is fast and scale well compared with the existing CP approach even in the sequential case, while significantly reducing the gap with the best state-of-the-art specialized algorithm.

There has been significant interest in the study of the problem of community search in large networks. Given one or more query nodes, this problem aims to discover densely connected subgroups containing these nodes. Various algorithms have been proposed to solve this challenging problem using different measures or a variety of cohesive subgraphs. In this paper, given an undirected graph and a set of query nodes, we study the community search using novel several cohesive subgraph models. More precisely, we propose to exploit several cohesive structures in a unified framework to find densely communities for query nodes in large complex networks. First, we review some existing cohesive structures. Next, to make these structures more effective models of communities, we focus on interesting configurations that are larger and more cohesive by fulfilling some constraints. The new structures obtained allow to ensure a larger density on the discovered communities and overcome some weaknesses of existing models. Finally, empirical results show the effectiveness of our framework to find communities for query nodes in a variety of real graphs.

Database users can be frustrated by having an empty answer to a query. In particular, querying RDF triple-stores are prone to failure due to the nature of RDF data. The problem of query relaxation is thus a helpful technique for efficiently querying RDF databases by providing users with alternative answers instead of an empty result. The main shortcoming of most prior researches is that they focus on the relaxation itself rather than the causes of failure. Yet, determining possible explanations, i.e. diagnoses, for an unexpected behavior of the system under observation is crucial to the user. In this paper, we present CADER, a novel approach for computing relaxations for failed queries over RDF databases. We show how the number of required database queries for determining all the possible relaxations can be limited to the search of failed subqueries of the user query. Then, we point out how the hitting set problem can be applied for determining the possible relaxed queries in an efficient way without querying the RDF database. Finally, the efficiency and scalability of CADER against existing solutions are shown through extensive experiments on the well-known RDF benchmarks with a variety of queries of different shapes.

Discovering the latent community structure is crucial to understanding the features of networks. Several approaches have been proposed to solve this challenging problem using different measures or data structures. Among them, detecting overlapping communities in a network is an usual way towards network structure discovery. It presents nice algorithmic issues, and plays an important role in complex network analysis. In this paper, we propose a new approach to detect overlapping communities in large complex networks. First, we introduce a novel subgraph concept based on triangles to capture the cohesion in social interactions, and propose an efficient approach to discover clusters in networks. Next, we show how the problem of detecting overlapping communities can be expressed as a Partial Max-SAT optimization problem. Our comprehensive experimental evaluation on publicly available real-life networks with ground-truth communities demonstrates the effectiveness and efficiency of our proposed method.

In this paper, we propose an efficient overlapping community detection method using a seed set expansion approach. In particular, we make an original use of a particular concept of graph theory, called chordal graph, to discover densely connected structures in social interactions based on maximal cliques. Indeed, a chordal graph possesses a number of interesting and useful properties that can help us to efficiently recover all maximal cliques of a given graph. Then, we develop new seeding strategies based on different fitness functions for discovering meaningful communities. Experimental results demonstrate the effectiveness and the efficiency of our overlapping community model in a variety of real graphs.

In the encoding of many real-world problems to propositional satisfiability, the cardinality constraint is a recurrent constraint that needs to be managed effectively. Several efficient encodings have been proposed while missing that such a constraint can be involved in a more general propositional formula. To avoid combinatorial explosion, the Tseitin principle usually used to translate such general propositional formula to Conjunctive Normal Form (CNF), introduces fresh propositional variables to represent sub-formulas and/or complex contraints. Thanks to Plaisted and Greenbaum improvement, the polarity of the sub-formula Φ is taken into account leading to conditional constraints of the form y → Φ, or Φ → y, where y is a fresh propositional variable. In the case where Φ represents a cardinality constraint, such translation leads to conditional cardinality constraints subject of the present paper. We first show that when all the clauses encoding the cardinality constraint are augmented with an additional new variable, most of the well-known encodings cease to maintain the generalized arc-consistency property. Then, we consider some of these encodings and show how they can be extended to recover such important property. An experimental validation is conducted on a SAT-based pattern mining application, where such conditional cardinality constraints are a cornerstone, showing the relevance of our proposed approach.

Behavioral consistency of cloud architectures is one of the pivotal challenges in cloud computing. In this paper, we propose a new approach for checking the behavioral consistency of the topology and orchestration of cloud computing. To do so, we choose TOSCA language in order to describe the cloud application. Then, we exploit the Wright ADL that encompasses the CSP language to check the consistency of cloud architectures using FDR2 model-checker.

Service Component Architectures (SCA) is widely used for the integration of heterogeneous applications. This heterogeneity, added to the distributed aspect of SCA, can be a source of behavioral mismatches. In this paper, we present a new approach for behavioral verification of SCA software architectures. More precisely, we propose a translation of a SCA source model to a Wright ADL configuration. In order to facilitate this translation, a guiding script and translation rules are introduced. Then, by using the wr2fdr tool, the translation of this wright configuration to a CSP specification is done. Finally, the FDR2 model-checker simulates and checks the obtained specification.

Ontologies can represent knowledge in a structured and formally well-understood way, which is crucial for information sharing. However, in practice, it is often difficult to have an error-free ontology. Conflicts can occur due to modeling errors or ontology merging and evolution. Moreover, uncertainty can happen because of modeling choices or the lack of confidence for a constructed ontology. Argumentation frameworks for knowledge bases reasoning and management have received extensive interests in the field of Artificial Intelligence in recent years. In this paper, we propose a unified framework to handle conflicts in uncertain ontologies with the use of deductive argumentation. Different from existing approaches, we introduce a stronger notion of conflict that covers both inconsistency and incoherence, where the latter is a special contradiction that can occur in an ontology. The unified approach spreads uncertainty degrees throughout argumentation trees and the enriched argument structure leads us to two novel inference relations. We then present a method to compute (counter)-arguments as well as argumentation trees in the context of uncertain ontologies based on the developments of three notions called minimal conflicting subontologies, maximal nonconflicting subontologies, and prudent justifications.

Currently, much research looks at treating the behavior properties beginning with the architectural design phase in SCA (Software Component Architectures) based applications. In this paper,we propose to map SCA onto the Wright ADL in order to verify the behavioral consistency of SCA software architectures. To achieve this goal, we suggest translating this source software architecture into a Wright configuration. Using Wr2fdr tool, this Wright configuration can be automatically translated to a CSP specification acceptable by the FDR2 model-checker.

How to succinctly represent the truly relevant information in big data graphs? The approach presented in this paper aims to discover hidden graph structures and exploit them to compactly summarize large graphs. First, we show that some special graph classes such as cliques and bicliques can be represented efficiently as Pseudo-Boolean (PB) constraints. Then, we propose three new graph classes representable as PB constraints, called nested, sequence and clique-nested bi-partite graphs. Finally, we derive a general approach for partial or complete summarization of an arbitrary graph as a disjunction of PB constraints. Our representation can be seen as an original way to represent the edges of the graph, as they correspond to particular solutions of the PB constraints. An extensive experimental evaluation on several real-world networks shows that our framework is competitive with the state-of-the-art compression technique.

Formal argumentation has received a lot of attention during the last two decades, since abstract argumentation framework provides the basis for various reasoning problems in Artificial Intelligence. Unfortunately, the exponential number of its possible semantics extensions makes some reasoning problems intractable in this framework. In this paper, we investigate the pivotal issue of efficient computation of acceptable arguments called extensions according to a given semantics. In particular, we address this aspect by applying a strategy of how to use preferences at the semantics level in order to determine what are “desirable” outcomes of the argumentation process. Then, we present a new approach for computing the Top-k extensions of an abstract argumentation framework, according to a user-specified preference relation. Indeed, an extension is a Top-k extension for a given semantics if it admits less than k extensions preferred to it with respect to a preference relation. Our experiments on various datasets demonstrate the effectiveness and scalability of our approach and the accuracy of the proposed enumeration method.

International audience

Discovering useful patterns plays an essential role in data management and data mining. Frequent itemset mining in uncertain transaction databases semantically and computationally differs from traditional techniques applied on (standard) precise transaction databases. Uncertain transaction databases consist of sets of existentially uncertain items. The uncertainty of items in transactions makes traditional techniques in applicable. Recent works propose interesting SAT-based encodings for the problem of discovering frequent itemsets in deterministic transaction databases. Our aim in this work is to extend the SAT-based encoding of frequent itemset mining to uncertain databases. Then, we propose a novel declarative mining frame-work for extracting uncertain frequent patterns from uncertain transaction databases. It makes an original use of constraints relaxation to obtain upper bounds to the expected support of frequent patterns, while guaranteeing the enumeration of all frequent itemsets with no false negatives. We experimentally evaluated our approach. The experimental results on real and synthetic data sets demonstrate the effectiveness of our proposal in mining frequent patterns.

Measuring inconsistency is recognized as an important issue for handling inconsistencies [5, 6]. Based on prime implicates canonical representation, we first characterize the conflicting variables allowing us to refine an existing inconsistency measure. Secondly, we propose a new measure, to circumscribe the internal conflicts in a knowledge base. This measure is proved to satisfy a new but weaker form of dominance.

Measuring inconsistency is recognized as an important issue for handling inconsistencies. Good measures are supposed to satisfy a set of rational properties. However, defining sound properties is sometimes problematic. In this paper, we emphasize one such property, named dominance, rarely satisfied by syntactic measures. Based on prime implicates canonical representation, we first characterize the conflicting variables allowing us to refine an existing inconsistency measure. Secondly, we propose a new measure, to circumscribe the internal conflicts in a knowledge base. This measure is proved to satisfy a new but weaker form of dominance.

This paper is intended to lay down the basic foundations of logic-based argumentation for reasoning about bounded resources. First, a simple variant of Boolean logic is introduced, allowing us to reason about consuming resources. An adapted tableau method is presented as a means for automated reasoning in the logic. Then, the main concepts of logic-based argumentation are revisited in this framework.