High-Utility Itemset Mining (HUIM) aims to discover itemsets whose utility exceeds a given threshold. While specialized algorithms achieve strong performance, they lack flexibility when additional domain constraints must be incorporated. Constraint Programming (CP) offers a declarative alternative, but requires strong propagation to remain competitive. In this paper, we propose a CP framework for utility-driven pattern mining based on a parameterized global constraint that unifies the enumeration of High-Utility Itemsets (HUIs) and a new condensed representation called Utility-Peak Itemsets (UPIs). A UPI is an itemset whose utility is greater or equal than that of all its immediate subsets and supersets, capturing locally utility-maximal patterns. We study the computational complexity of UPI mining and show that deciding whether a high-utility UPI exists, for a given utility threshold, is NP-complete. Our global constraint, PeakUtility, integrates utility computation and upper-bound pruning through propagation rules. Experiments demonstrate that our approach performs competitively with the state of the art HUIM algorithms while preserving the modelling flexibility of CP.

Migrants traversing geographically distinct routes such as the Trans-Saharan and Balkan corridors often recount strikingly parallel lived experiences: police violence, smuggler exploitation, dangerous crossings, and family separation. We introduce the task of experiential intertextuality detection: automatically identifying shared experiential echoes across migration narratives without requiring annotated training data. From 108 French migration narratives spanning both corridors, we automatically generate sentence pairs and score them using annotation-free methods: lexical baselines, sentence embeddings, POS-based structural features, a migration-specific theme lexicon, context-aware narrative features, and zero-shot LLM scoring with Qwen2.5-7B and Mistral-7B under three prompting strategies. We validate all methods against 816 expertannotated intertextuality judgments (interannotator Krippendorff’s α=0.27). Our results reveal that all surface, structural, and embedding methods correlate only weakly with expert judgments (r≤0.30); Qwen2.5-7B zero-shot achieves the best single-method correlation (r=0.38); few-shot examples degrade Qwen but dramatically improve Mistral; narrative position significantly predicts intertextuality, with departure-phase pairs showing the highest experiential echoes; and a supervised hybrid combining all 31 features achieves r=0.45, a 21% improvement over the best individual method.

ABSTRACT We propose an incremental similarity‐based label propagation algorithm (DLPA‐S) for detecting dynamic community structures. As the network evolves, the method efficiently updates the communities over time via local label updates driven by changes in network topology—including edge and vertex additions or removals—and vertex similarity. This incremental approach significantly reduces computational cost while preserving accuracy in capturing community evolution. We evaluate DLPA‐S using a comprehensive set of quality metrics that assess both the structural properties of the network and the agreement between detected communities and ground‐truth partitions. Experiments are conducted on synthetic and real‐world dynamic networks, varying key graph characteristics such as the number of vertices and the average degree, as well as across diverse community scenarios. The results show that DLPA‐S consistently achieves stable and high‐performing results, maintains high NMI and F1 scores, ensures strong internal connectivity, clear community separability, and avoids disconnected communities, while remaining computationally efficient.

Random Forests (RFs) are one of the most popular classifiers in machine learning. RF is an ensemble learning method that combines multiple Decision Trees (DTs), providing a more robust and accurate model than a single DT. However, one of the main step of RFs is the random selection of many different features during the construction phase of DTs, resulting in a forest with various features, which makes it difficult to extract short and concise explanations. In this paper, we propose integrating Logical Analysis of Data (LAD) into RFs. LAD is a pattern learning framework that combines optimization, Boolean functions, and combinatorial theory. One of its main goals is to generate minimal support sets (MSSes) that discriminate between different groups of data. More precisely, we show how to enhance the classical RF algorithm by randomly choosing MSSes rather than randomly choosing feature subsets that potentially contain irrelevant features for constructing DTs. Experiments on benchmark datasets reveal that integrating LAD into classical RFs using MSSes can maintain similar performance in terms of accuracy, produce forests of similar size, reduce the set of used features, and enable the extraction of significantly shorter explanations compared to classical RFs.

The curse of dimensionality presents a significant challenge in data mining, pattern recognition, computer vision, and machine learning applications. Feature selection is a primary approach to address this challenge. It aims to eliminate irrelevant and redundant features while preserving the relevant ones to reduce computation time, improve prediction performance, and enhance the understanding of data. In this paper, we introduce a new feature selection (FS) technique based on the Logical Analysis of Data (LAD), a pattern learning framework that combines optimization, Boolean functions, and combinatorial theory. One of its main objectives is to generate minimal support sets of features (subsets of features) that discriminate between different groups of data. To generate such subsets, we first reduce the complexity of the LAD optimization task by transforming it into the problem of enumerating minimal hitting sets in a hypergraph, for which efficient implementations exist. Those feature subsets are then ranked based on a scoring method before selecting the highest quality one. Moreover, we explore the relationship between optimal Decision Trees (DTs) and LAD-based FS, introducing new optimality criteria, namely DTs involving a minimum number of features. Finally, we conduct comparative evaluations of LAD-based approach against several state-of-the-art (SOTA) FS methods on benchmark datasets, including two-class binary datasets and numerical datasets with two and multiple classes. Experiments reveal that our approach is competitive with SOTA methods, selecting high-quality feature subsets that maintain or enhance the performance of DTs and other classifiers like SVM, KNN, and Naive Bayes.

International audience

On a worldwide scale, an increasing number of victims of human trafficking were observed these last years, covering a majority of countries and territories. Among them, a large portion of women and girls are recruited primarily for sexual exploitation. United Nations Office on Drugs and Crime (UNODC) highlights the difficulties of access to justice which deprive victims of protection, a central issue behind our work. Our contribution is part of an emerging research trend, combining Artificial Intelligence (AI), Humanities and Social Sciences (HSS). It makes an original use of legal database to identify Human Trafficking Networks (HTNs), involving both sexual abuse victims and exploiters. First, a reformulation of the legal database as a numerical database is proposed, using new features expressing relationships between people involved in the same court case, likely to better reveal HTNs. Secondly, six machine learning algorithms, including Decision Tree, Random Forest, Gradient Boosting, Logistic Regression, Support Vector Machine (SVM) and K-Nearest Neighbors (KNN) are used to train on numerical database and learn to classify the input court case into one of the three classes: Not suspicious, Suspicious, or Probably suspicious. We in details discuss knowledge-based feature engineering, dataset balancing, parameters tuning, and best models selection. The comparative empirical evaluations between those classification algorithms have been conducted in order to highlights the relevance of our HTNs detection approach. To help the end-users, to better understand the displayed HTNs, for Decision Tree and Random Forest, we also provide explanations of why such court case can be classified. Those results were finally discussed with experts in the field of human trafficking, providing us with interesting feedback shedding light to this multidimensional form of modern-day slavery problem.

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

Gradual itemsets model complex attributes covariation of the form "The more or less is A, the more or less is B". Recently, such kind of itemsets have received attention from the data mining community, where several formalizations and methods have been defined to automatically extract and maintain gradual patterns from numerical databases. However, mining gradual itemsets remains challenging as the task is more complex than ordering the transactions according to several dimensions or attributes. In fact, the order in which attributes are considered impacts the sorting operation. One can note that an ordering of the transactions according to a single attribute leads to a sequence of itemsets where items correspond to transaction identifiers. In this paper and from this observation, we propose a new formulation of the gradual itemset mining task as the problem of sequential pattern mining. This original reduction allows us to exploit sequential pattern mining algorithms to extract gradual itemsets. Experimental results obtained on several numerical datasets show the feasibility of our proposed framework.

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.

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.

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.

Measuring inconsistency is recognized as an important research issue for quantifying and handling inconsistencies in knowledge bases. Several logic-based inconsistency measures have been proposed. Minimal unsatisfiable and maximal satisfiable subsets are at the heart of the syntactic measures, while semantic inconsistency measures are often based on some paraconsistent semantics. In order to design interesting measures faithful to human rationality, many properties have been introduced to reach this goal. In this paper, we propose a new property called sub-additivity allowing to push further the ability to reorder knowledge bases according to their inconsistency degree. After pointing out the limitations of several measures to satisfy the sub-additivity property, we present a new measure based on a fine exploitation of the internal structure of the knowledge base, namely the structure of its associated minimal unsatisfiable subsets. Then, we show how its computation can be formulated as a nonlinear optimization problem. Finally, we prove that the new measure satisfies all the required properties while highlighting its interesting features.

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.

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.

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.

An extension and several variants of Dalal's Quad polynomial fragments of SAT are presented. Firstly, the stability of Quad fragments is investigated. Then, the extension is as follows. Quad fixed total orderings of clauses is accompanied with specific additional separate orderings of maximal sub-clauses. Interestingly, the resulting fragments extend Quad without degrading its worst-case complexity. Several other variants of Quad that give rise to additional different polynomial fragments are then investigated.

Conflict based clause learning is known to be an important component in Modern SAT solving. Because of the exponential blow up of the size of learnt clauses database, maintaining a relevant and polynomially bounded set of learnt clauses is crucial for the efficiency of clause learning based SAT solvers. In this paper, we first compare several criteria for selecting the most relevant learnt clauses with a simple random selection strategy. We then propose new criteria allowing us to select relevant clauses w.r.t. A given search state. Then, we use such strategies as a means to diversify the search in a portfolio based parallel solver. An experimental evaluation comparing the classical Many SAT solver with the one augmented with multiple deletion strategies, shows the interest of such approach.

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.

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.

This paper presents a dynamic substitution technique of Boolean functions. It first recovers a set of Boolean functions from Boolean formula in conjunctive normal form (CNF). Then these functions are used to reduce the size of the learnt clauses by substituting the input arguments by the output ones. Preliminary experiments show the feasibility of our approach on some classes of SAT instances taken from the recent SAT Race and competitions.

In this paper a learning based local search approach for propositional satisfiability is presented. It is based on an original adaptation of the conflict driven clause learning (CDCL) scheme to local search. First an extended implication graph for complete assignments of the set of variables is proposed. Secondly, a unit propagation based technique for building and using such implication graph is designed. Finally, we show how this new learning scheme can be integrated to the state-of-the-art local search solver WSAT. Interestingly enough, the obtained local search approach is able to prove unsatisfiability. Experimental results show very good performances on many classes of SAT instances from the last SAT competitions.

In this paper, a semantic generalization of neighbourhood substitutability is presented. Instead of the syntactical concept of supports, our generalization originally exploits a new semantic measure based on Single Arc-Consistency (SAC) checking. This generalization is then exploited in two different ways. Firstly, a new pretreatment of constraints networks is proposed. Secondly, as SAC is a basic operation in backtrack search-based algorithms like $\MAC$, we show that our generalization can be easily applied dynamically. The experimental results of our approach show interesting improvements on some classes of $\CSP$ instances and demonstrate the feasibility of the dynamic integration of our generalized neighbourhood substitutability.

In this paper an original dynamic partition of formu- lae in Conjunctive Normal Form (CNF) is presented. It is based on the autarky concept first introduced by Monien and Speckenmeyer and further investigated by Kullmann and Van Gelder. Intuitively, an autarky is a partial assign- ment satisfying some clauses while not affecting any literal in any other clause, leading to a partition of the CNF for- mula. Autarkies can play a dramatic role in the efficiency of modern SAT solvers. The approach in this paper aims to dy- namically extend the current partial assignment to a local autarky thanks to an inference rule based on unit propaga- tion. More precisely, at each node of the search tree, it is checked whether the current decision literal can be made monotone by subsuming all the clauses where it appears negatively. The formal framework is detailed and its techni- cal features discussed.

This paper presents an original dynamic subsumption technique for Boolean CNF formulae. It exploits simple and sufficient conditions to detect, during conflict analysis, clauses from the formula that can be reduced by subsumption. During the learnt clause derivation, and at each step of the associated resolution process, checks for backward subsumption between the current resolvent and clauses from the original formula are efficiently performed. The resulting method allows the dynamic removal of literals from the original clauses. Experimental results show that the integration of our dynamic subsumption technique within the state-of-the-art SAT solvers Minisat and Rsat particularly benefits to crafted problems.

In this paper, we propose a new technique to compute irredundant sub-sets of constraint networks. Since, checking redundancy is Co-NP Complete problem, we use different polynomial local consistency entailments for reducing the computational complexity. The obtained constraint network is irredundant modulo a given local consistency. Redundant constraints are eliminated from the original instance producing an equivalent one with respect to satisfiability. Eliminating redundancy might help the CSP solver to direct the search to the most constrained (irredundant) part of the network.

In this paper, we present a new way to preprocess Boolean formulae in Conjunctive Normal Form (CNF). In contrast to most of the current pre-processing techniques, our approach aims at improving the filtering power of the original clauses while producing a small number of additional and relevant clauses. More precisely, an incomplete redundancy check is performed on each original clauses through unit propagation, leading to either a sub-clause or to a new relevant one generated by the clause learning scheme. This preprocessor is empirically compared to the best existing one in terms of size reduction and the ability to improve a state-of-the-art satisfiability solver.

Many local consistency properties have been exploited in solving constraint satisfaction problems. The objective is to reduce the search space and consequently improve search methods. It has been shown that maintaining arc- consistency during search is very useful in solving CSPs. The use of stronger local consistency forms (like path consistency) is still limited since they need complicated data structures to be managed and the constraint graph may be modified. In this paper, we propose a possible way to get benefits from using, in a preprocessing step, a partial form of path consistency and arc consistency based on support intervals notion.

In this paper, a new approach for computing strong backdoor sets of Boolean formula in conjunctive normal form (CNF) is proposed. It makes an original use of local search techniques for finding an assignment leading to a largest renamable Horn sub-formula of a given CNF. More precisely, at each step, preference is given to variables such that when assigned to the opposite value lead to the smallest number of remaining non-Horn clauses. Consequently, if no positive or non Horn clauses remain in the formula, our approach answer the satisfiability of the original formula; otherwise, a smallest non-Horn sub-formula is used to extract the set of variables (strong backdoor) such that when assigned leads to a tractable sub-formula. Branching on the variables of the strong backdoor set leads to significant improvements of Zchaff SAT solver with respect to many real worlds SAT instances

Solving quantified Boolean formulas (QBF) has become an attractive research area in artificial intelligence. Many important artificial intelligence problems (planning, nonmonotonic reasoning, formal verification, etc.) can be reduced to QBFs. A new DLL-based method is proposed that integrates binary decision diagram (BDD) to set free the variable ordering heuristics that are traditionally constrained by the static order of the QBF quantifiers. BDD is used to represent in a compact form the set of models of the Boolean formula. Interesting reduction operators are proposed in order to dynamically reduce the BDD size and to answer the validity of the QBF. Experimental results on instances from the QBF'03 evaluation show that our approach can efficiently solve instances that are very hard for current QBF solvers.

Many backtrack search algorithms has been designed over the last years to solve constraint satisfaction problems. Among them, Forward Checking (FC) and Maintaining Arc Consistency (MAC) algorithms are the most popular and studied algorithms. In This work, such algorithms are revisited and extensively compared giving rise to interesting characterization of their efficiency with respect to random instances. More precisely, we provide experimental evidence that FC outperforms MAC on hard CSPs with high graph density and low constraint tightness whereas MAC is better on hard CSPs with low density and high constraints tightness. This results show that on some CSPs maintaining full arc consistency during search might be time consuming. Then, we propose a new generic approach that maintain partial and parameterizable form of local consistency.

Conflict analysis is a powerful paradigm of backtrack search algorithms, in particular for solving satisfiability problems arising from practical applications. Accordingly, most recent Boolean satisfiability solvers implement forms of conflict analysis, at least to some extent. In this paper, a branching criterion initially introduced by Purdom is revisited and extended. Contrary to the author's a priori analysis, it is shown very efficient from a practical point of view in that it allows search trees in SAT solving to be pruned in a significant way while obeying an interesting time and space trade-off. More precisely, we show that redundancies during the search process can be avoided without adding new constraints explicitly. Moreover, the technique can be used not only to prune branches in the search tree, but also to derive implied literals. Extensive experimental results illustrate the feasibility and practical interest of this approach.

In this paper, the use of local search to validate first-order knowledge-based systems is investigated. It is well known that such techniques can prove efficient in showing that consistency constraints do hold, at least in the propositional case. Powerful heuristics about the trace of local search allow proofs of inconsistency to be obtained as well. However, how local search can be applied to first-order knowledge bases without giving rise to a combinatorial space explosion remains an open issue. In this paper, a partial instantiation schema is proposed in the context of the incremental consistency–inconsistency problem. It allows forms of depth-limited consistency and inconsistency to be handled in an effective manner, showing promising paths for the development of new efficient consistency checking techniques for first-order knowledge bases. © 2001 John Wiley & Sons, Inc.

Local consistency is often a suitable paradigm for solving constraint satisfaction problems. We show how search algorithms could be improved, thanks to a smart use of two filtering techniques (path consistency and singleton arc consistency). We propose a possible way to get benefits from using a partial form of path consistency (PC) during the search. We show how local treatment based on singleton arc consistency (SAC) can be used to achieve more powerful pruning.

In this paper, we address a fundamental problem in the formalization and implementation of cooperative knowledge bases: the difficulty of preserving consistency while interacting or combining them. Indeed, knowledge bases that are individually consistent can exhibit global inconsistency. This stumbling-block problem is an even more serious drawback when knowledge and reasoning are expressed using logical terms. Indeed, on the one hand, two contradictory pieces of information lead to global inconsistency under complete standard rules of deduction: every assertion and its contrary can be deduced. On the other hand, checking the logical consistency of a propositional knowledge base is an NP-complete problem and is often out of reach for large real-life applications. In this paper, a new practical technique to locate inconsistent interacting pieces of information is presented in the context of cooperative logical knowledge bases. Based on a recently discovered heuristic about the work performed by local search techniques, it can be applied in the context of large interacting knowledge bases.