International audience

In this paper, we introduce a syntactic framework for analyzing and handling inconsistencies in propositional bases. Our approach focuses on examining the relationships between variable occurrences within conflicts. We propose two dual concepts: Minimal Inconsistency Relation (MIR) and Maximal Consistency Relation (MCR). Each MIR is a minimal equivalence relation on variable occurrences that results in inconsistency, while each MCR is a maximal equivalence relation designed to prevent inconsistency. Notably, MIRs capture conflicts overlooked by minimal inconsistent subsets. Using MCRs, we develop a series of non-explosive inference relations. The main strategy involves restoring consistency by modifying the propositional base according to each MCR, followed by employing the classical inference relation to derive conclusions. Additionally, we propose an unusual semantics that assigns truth values to variable occurrences instead of the variables themselves. The associated inference relations are established through Boolean interpretations compatible with the occurrence-based models.

In formal methods, checking the validity of some proof obligations results in reasoning about sets, and particularly their interrelations and their cardinalities. Motivated by this interest, we investigate hybrid problems that combine constraints from both aspects. In this context, we consider two approaches: one purely qualitative and one explicitly representing membership. We propose SAT-based encodings for solving these problems. First we encode qualitative constraints on relations between sets and their cardinalities. Afterwards, we deal with richer constraints on set elements and with numerical constraints on both cardinalities and integer variables, assuming a fixed domain. In this setting, we identify a domain size bound for the version with explicit membership, beyond which increasing the domain cannot affect satisfiability. We evaluate the proposed encodings on real-world B language specifications. The proposed approaches allow the validation of proofs not yet decided by several existing approaches, and so could be used in addition to the others in order to automate the validation of even more proofs.

This paper introduces a game-theoretic framework for restoring consistency in propositional bases. The process is modeled as an interactive dialogue between two agents: a Proponent, who seeks to isolate a unique, consistent subset by posing strategic questions, and an Opponent, who aims to obstruct that goal through adversarial responses. We show that this framework provides a foundation for quantifying the effort involved in restoring consistency, revealing a connection between this effort and entropy in information theory. Focusing on the case where consistency is achieved by isolating a single maximal consistent subset, we establish links between the structure and number of such subsets and the existence of winning strategies. Finally, we demonstrate how the quantified restoration effort can serve as a basis for measuring inconsistency.

Inconsistency handling is a fundamental problem in knowledge representation and reasoning. In this paper, we study this problem in the context of qualitative spatio-temporal reasoning, a framework for reasoning about space and time in a symbolic, human-like manner, by following an approach similar to that used for defining paraconsistent logics; paraconsistency allows deriving informative conclusions from inconsistent knowledge bases by mainly avoiding the principle of explosion. Inspired by paraconsistent logics, such as Priest’s logic LPm, we introduce the notion of paraconsistent scenario (i.e., a qualitative solution), which can be seen as a scenario that allows a conjunction of base relations between two variables, e.g., x precedes ∧ follows y. Further, we present several interesting theoretical properties that concern paraconsistent scenarios, including computational complexity results, and describe two distinct approaches for computing paraconsistent scenarios and solving other related problems. Moreover, we provide implementations of our two methods for computing paraconsistent scenarios and experimentally evaluate them using different strategies/metrics. Finally, we show that our paraconsistent scenario notion allows us to adapt to qualitative reasoning one of the well-known inconsistency measures employed in the propositional case, namely, contension measure.

Decomposition can be a fundamental process for dealing with inconsistency in different domains. Among other things, it allows us to capture potential contexts, identify conflicting factors, restore consistency, and measure inconsistency. The aim of this paper is to explore the process of decomposition in qualitative spatial and temporal reasoning. We first study a problem that consists in decomposing the original inconsistent constraint network into the fewest possible consistent subnetworks (components) that share a given part. After establishing several interesting theoretical properties, such as providing bounds on the number of components in a decomposition, as well as computational complexity results, we propose two methods for solving this problem. The first method is based on a SAT encoding, while the second one corresponds to a greedy constraint-based algorithm, a variant of which involves the use of spanning trees to reduce the number of oracle calls. Secondly, we consider a version of the previous decomposition problem by focusing on maximizing the similarity between the decomposition components; the similarity in this context is represented by the common constraints among components. We then adapt our methods to solve this new problem. Thirdly, we propose two inconsistency measures that are based on our decomposition framework and show that they satisfy several desired properties. Finally, we provide implementations of our decomposition methods and perform an experimental evaluation.

The concept of prime implicant is a fundamental tool in Boolean algebra, which is used in Boolean circuit design and, recently, in explainable AI. This study investigates an analogous concept in qualitative spatial and temporal reasoning, called prime scenario. Specifically, we define a prime scenario of a qualitative constraint network (QCN) as a minimal set of decisions that can uniquely determine solutions of this QCN. We propose in this paper a collection of algorithms designed to address various problems related to prime scenarios. The first three algorithms aim to generate a prime scenario from a scenario of a QCN. The main idea consists in using path consistency to identify the constraints that can be ignored to generate a prime scenario. The next two algorithms focus on generating a set of prime scenarios that cover all the scenarios of the original QCN: The first algorithm examines every branch of the search tree, while the second is based on the use of a SAT encoding. Our last algorithm is concerned with computing a minimum-size prime scenario by using a MaxSAT encoding built from countermodels of the original QCN. We show that this algorithm is particularly useful for measuring the robustness of a QCN. Finally, a preliminary experimental evaluation is performed with instances of Allen’s Interval Algebra to assess the efficiency of our algorithms and, hence, also the difficulty of the newly introduced problems here.

Dealing with inconsistency is a central problem in AI, due to the fact that inconsistency can arise for many reasons in real-world applications, such as context dependency, multi-source information, vagueness, noisy data, etc. Among the approaches that are involved in inconsistency handling, we can mention argumentation, non-monotonic reasoning, and paraconsistency, e.g., see [Philippe Besnard and Anthony Hunter, 2008; Gerhard Brewka et al., 1997; Koji Tanaka et al., 2013]. In the work of [Yakoub Salhi and Michael Sioutis, 2023], we are interested in dealing with inconsistency in the context of Qualitative Spatio-Temporal Reasoning (QSTR) [Ligozat, 2013]. QSTR is an AI framework that aims to mimic, natural, human-like representation and reasoning regarding space and time. This framework is applied to a variety of domains, such as qualitative case-based reasoning and learning [Thiago Pedro Donadon Homem et al., 2020] and visual sensemaking [Jakob Suchan et al., 2021]; the interested reader is referred to [Michael Sioutis and Diedrich Wolter, 2021] for a recent survey. Motivation. In [Yakoub Salhi and Michael Sioutis, 2023], we study the decomposition of an inconsistent constraint network into consistent subnetworks under, possible, mandatory constraints. To illustrate the interest of such a decomposition, we provide a simple example described in Figure 1. The QCN depicted in the top part of the figure corresponds to a description of an inconsistent plan. Further, we assume that the constraint Task A {before} Task B is mandatory. To handle inconsistency, this plan can be transformed into a decomposition of two consistent plans, depicted in the bottom part of the figure; this decomposition can be used, e.g., to capture the fact that Task C must be performed twice. More generally, network decomposition can be involved in inconsistency handling in several ways: it can be used to identify potential contexts that explain the presence of inconsistent information; it can also be used to restore consistency through a compromise between the components of a decomposition, e.g., by using belief merging [Jean-François Condotta et al., 2010]; in addition, QCN decomposition can be used as the basis for defining inconsistency measures. Contributions. We summarize the contributions of [Yakoub Salhi and Michael Sioutis, 2023] as follows. First, we propose a theoretical study of a problem that consists in decomposing an inconsistent QCN into a bounded number of consistent QCNs that may satisfy a specified part in the original QCN; intuitively, the required common part corresponds to the constraints that are considered necessary, if any. To this end, we provide upper bounds for the minimum number of components in a decomposition as well as computational complexity results. Secondly, we provide two methods for solving our decomposition problem. The first method corresponds to a greedy constraint-based algorithm, a variant of which involves the use of spanning trees; the basic idea of this variant is that any acyclic constraint graph in QSTR is consistent, and such a graph can be used as a starting point for building consistent components. The second method corresponds to a SAT-based encoding; every model of this encoding is used to construct a valid decomposition. Thirdly, we consider two optimization versions of the initial decomposition problem that focus on minimizing the number of components and maximizing the similarity between components, respectively. The similarity between two QCNs is quantified by the number of common non-universal constraints; the interest in maximizing the similarity lies mainly in the fact that it reduces the number of constraints that allow each component to be distinguished from the rest. Of course, our previous methods are adapted to tackle these optimization versions, too. Additionally, we introduce two inconsistency measures based on QCN decomposition, which can be seen as counterparts of measures for propositional KBs introduced in [Matthias Thimm, 2016; Meriem Ammoura et al., 2017], and show that they satisfy several desired properties in the literature. Finally, we provide implementations of our methods for computing decompositions and experimentally evaluate them using different metrics.

Qualitative reasoning formalisms facilitate the representation and interpretation of information involving complex entities. We use in this paper qualitative spatial and temporal reasoning to introduce novel data mining tasks, which consist in extracting knowledge from quantitative databases that are trans-formed into collections of qualitative relation networks (QRNs). After describing our qualitative data mining framework, we first propose an Apriori-like algorithm that exploits monotonicity and QRN consistency for pruning the search space: the validity of a pattern candidate depends on the supports of the larger patterns that include it and on its consistency. We then introduce an encoding of our data mining tasks into the well-known problem of frequent itemset mining. We finally show the feasibility of our approach by providing preliminary experimental results using real-world datasets about the movements of football players during matches.

One of the main aims of the methods developed for reasoning under inconsistency, in particular paraconsistent inference, is to derive informative conclusions from inconsistent bases. In this paper, we introduce an approach based on inconsistency measurement for defining non-monotonic paraconsistent consequence relations. The main idea consists in adapting properties of classical reasoning under consistency to inconsistent propositional bases by involving inconsistency measures (IM). We first exhibit interesting properties of our consequence relations. We then study situations where they bring about consequences that are always jointly consistent. In particular, we introduce a property of inconsistency measures that guarantees the consistency of the set of all entailed formulas. We also show that this property leads to several interesting properties of our IM-based consequence relations. Finally, we discuss relationships between our framework and well-known consequence relations that are based on maximal consistent subsets. In this setting, we establish direct connections between the latter and properties of inconsistency measures.

Information asymmetry occurs when an imbalance of knowledge exists between two parties, such as a buyer and a seller, a regulator and an operator, and an employer and an employee. It is a key concept in several domains, in particular, in economics. We propose in this work a general logic-based framework for measuring the information asymmetry between two parties. A situation of information asymmetry is represented by a knowledge base and a set of questions. We define the notion of information asymmetry measure through rationality postulates. We further introduce a syntactic concept, called minimal question subset (MQS), to take into consideration the fact that answering some questions allows avoiding others. This concept is used for defining rationality postulates and measures. Finally, we propose a method for computing the MQSes of a given situation of information asymmetry.

Formal logic can be used as a tool for representing complex and heterogeneous data such as beliefs, knowledge and preferences. This study proposes an approach for defining clustering methods that deal with bases of propositional formulas in classical logic, i.e., methods for dividing formula bases into meaningful groups. We first use a postulate-based approach for introducing an intuitive framework for formula clustering. Then, in order to characterize interesting clustering forms, we introduce additional properties that take into consideration different notions, such us logical consequence, overlapping, and consistent partition. Finally, we describe our approach that shows how the inconsistency measures can be involved in improving the task of formula clustering. The main idea consists in using the measures for quantifying the quality of the inconsistent clusters. In this context, we propose further properties that allow characterizing interesting aspects related to the amount of inconsistency.

Controlling access to knowledge plays a crucial role in many multi-agent systems. In- deed, it is related to different central aspects in interactions among agents such as privacy, security, and cooperation. In this paper, we propose a framework for dealing with access to knowledge that is based on the inference process in classical propositional logic: an agent has access to every piece of knowledge that can be derived from the available knowledge using the classical inference process. We first introduce a basic problem in which an agent has to hide pieces of knowledge, and we show that this problem can be solved through the computation of maximal consistent subsets. In the same way, we also propose a coun- terpart of the previous problem in which an agent has to share pieces of knowledge, and we show that this problem can be solved through the computation of minimal inconsis- tent subsets. Then, we propose a generalization of the previous problem where an agent has to share pieces of knowledge and hide at the same time others. In this context, we introduce several concepts that allow capturing interesting aspects. Finally, we propose a weight-based approach by associating integers with the pieces of knowledge that have to be shared or hidden.

In this paper, we aim at studying the Exactly-One-SAT problem (in short EO-SAT). This problem consists in deciding whether a given CNF formula admits a model so that each clause has exactly one satisfied literal. The contribution of this work is twofold. Firstly, we introduce a tractable class in EO-SAT, which is defined by a property that has to be satisfied by combinations of clauses. This class can be seen as a counterpart of tractable classes in the maximum independent set problem. Secondly, we propose graph-based approaches for reducing the number of variables and clauses of EO-SAT instances, which consequently allow for reducing the search space. We provide an experimental study for evaluating these approach by showing its interest in the context of the graph coloring problem.

In this paper, we introduce a new data mining framework that is based on qualitative reasoning. We consider databases where the item domains are of different types, such as numerical values, time intervals and spatial regions. Then, for the considered tasks, we associate to each item a constraint network in a qualitative formalism representing the relations between all the pairs of objects of the database w.r.t. this item. In this context, the introduced data mining problems consist in discovering qualitative covariations between items. In a sense, our framework can be seen as a generalization of gradual itemset mining. In order to solve the introduced problem, we use a declarative approach based on the satisfiability problem in classical propositional logic (SAT). Indeed, we define SAT encodings where the models represent the desired patterns.

In this article we define label-free sequent calculi for the intuitionistic modal logics obtained from the combinations of the axioms T , B , 4 and 5. These calculi are based on a multi-contextual sequent structure, called Tree-sequent, which allows us to define such calculi for such intuitionistic modal logics. From the calculi defined for the IK , IT , IB4 and ITB logics, we also provide new decision procedures and alternative syntactic proofs of decidability.

In this paper, we propose a new approach for defining tractable classes in propositional satisfiability problem (in short SAT). The basic idea consists in transforming SAT instances into instances of the problem of finding a maximum independent set. In this context, we only consider propositional formulæ in conjunctive normal form where each clause is either positive or binary negative. Tractable classes are obtained from existing polynomial time algorithms of the problem of finding a maximum independent set in the case of different graph classes, such as claw-free graphs and perfect graphs. We show, in particular, that the pigeonhole principle belongs to one of the defined tractable classes. Furthermore, we propose a characterization of the minimal models in the largest considered fragment based on the maximum independent set problem.

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.

We introduce a preferences-based itemset mining framework. Preferences are encoded by a penalty function over the transactions in a database. We define an itemset mining problem where we associate to each transaction a penalty value. This problem consists in generating the frequent itemsets with a maximum penalty threshold. We then provide a propositional satisfiability based encoding. We extend the previous problem with a penalty function over items, where we use two maximum penalty thresholds, over the transactions and over the items. In this setting, computing the optimum itemsets corresponds to computing Pareto front. The experimental evaluation on real world data shows the feasibility of our approach.

Frequent itemset mining (FIM) is a useful task for discovering frequent co-occurring items. Since its inception, a number of significant FIM algorithms have been developed to speed up mining performances. Unfortunately, for huge dataset, scalability remains an important issue. In this work, we propose a new propositional satisfiability (SAT) parallel approach, called PSATCFIM, to deal with closed frequent itemsets mining problem. It is designed to run on multicore machines and uses a divide and conquer approach to partition the enumeration process. Such partitioning based on guiding paths eliminates computational overlap between cores. Through empirical study, we demonstrate that PSATCFIM can achieve significant performance improvements with respect to the sequential based version.

In this paper, we propose an extension of our mining-based SAT compression framework to constraint satisfaction problem (CSP). We consider n-ary extensional constraints (table constraints). Our approach aims to reduce the size of the CSP by exploiting the structure of the constraints graph and its associated microstructure. More precisely, we apply itemset mining techniques to search for closed frequent itemsets on these two representations. Using Tseitin extension, we rewrite the whole CSP to another compressed CSP equivalent with respect to satisfiability. Our approach contrasts with the previous proposed technique by Katsirelos and Walsh, as it does not change the inner-structure of the constraints. Experiments on some CSP instances show that our approach can achieve interesting compression rate.

Dung's argumentation framework is an abstract framework based on a set of arguments and a binary attack relation defined over the set. One instantiation, among many others, of Dung's framework consists in constructing the arguments from a set of propositional logic formulas. Thus an argument is seen as a reason for or against the truth of a particular statement. Despite its advantages, the argumentation approach for inconsistency handling also has important shortcomings. More precisely, in some applications what one is interested in are not so much only the conclusions supported by the arguments but also the precise explications of such conclusions. We show that argumentation framework applied to classical logic formulas is not suitable to deal with this problem. On the other hand, intuitionistic logic appears to be a natural alternative candidate logic (instead of classical logic) to instantiate Dung's framework. We develop constructive argumentation framework. We show that intuitionistic logic offers nice and desirable properties of the arguments. We also provide a characterization of the arguments in this setting in terms of minimal inconsistent subsets when intuitionistic logic is embedded in the modal logic S4.

In this paper, we propose a SAT-based encoding for the problem of discovering frequent, closed and maximal patterns in a sequence of items and a sequence of itemsets. Our encoding can be seen as an improvement of the approach proposed in [8] for the sequences of items. In this case, we show experimentally on real world data that our encoding is significantly better. Then we introduce a new extension of the problem to enumerate patterns in a sequence of itemsets. Thanks to the flexibility and to the declarative aspects of our SAT-based approach, an encoding for the sequences of itemsets is obtained by a very slight modification of that for the sequences of items.

In this paper, we propose a first application of data mining techniques to propositional satisfiability. Our proposed mining based compression approach aims to discover and to exploit hidden structural knowledge for reducing the size of propositional formulae in conjunctive normal form (CNF). It combines both frequent itemset mining techniques and Tseitin's encoding for a compact representation of CNF formulae. The experimental evaluation of our approach shows interesting reductions of the sizes of many application instances taken from the last SAT competitions.

In this paper, we show how symmetries, a fundamental structural property, can be used to prune the search space in itemset mining problems. Our approach is based on a dynamic integration of symmetries in APRIORI-like algorithms to prune the set of possible candidate patterns. More precisely, for a given itemset, symmetry can be applied to deduce other itemsets while preserving their properties. We also show that our symmetry-based pruning approach can be extended to the general Mannila and Toivonen pattern mining framework. Experimental results highlight the usefulness and the efficiency of our symmetry-based pruning approach.