The enumeration of all Maximal Satisfiable Subsets (MSSes) or all Minimal Correction Subsets (MCSes) of an unsatisfiable CNF Boolean formula is a useful and sometimes necessary step for solving a variety of important A.I. issues. Although the number of different MCSes of a CNF Boolean formula is exponential in the worst case, it remains low in many practical situations; this makes the tentative enumeration possibly successful in these latter cases. In the paper, a technique is introduced that boosts the currently most efficient practical approaches to enumerate MCSes. It implements a model rotation paradigm that allows the set of MCSes to be computed in an heuristically efficient way.

The search for one consensus that reconciles several conflicting agents or information sources is a key paradigm in both everyday-life and A.I. In this paper, we improve a recent approach to consensus-finding that has been developed in the Boolean logic framework. In that recent approach consensuses are defined as being some specific non-conflicting fragments of the set-theoretic union of all the information to be mitigated. In order to be a consensus, such a fragment must be conflict-free with every information source, taken individually. That approach has also introduced a generic method to compute one consensus that obeys various possible maximality criteria, including maximality with respect to set-theoretical inclusion, i.e., max⊆ consensuses. As max⊆ consensuses are of clear interest, the focus is on their computation in this paper. We develop an algorithm for computing one max⊆ consensus that is experimentally more time and space efficient than the computational method proposed in the initial study.

The efficient extraction of one maximal information subset that does not conflict with multiple contxts or additional information sources is a key basic issue in many A.I. domains, especially when these contexts or sources can be mutually conflicting. In this paper, this question is addressed from a computational point of view in clausal Boolean logic. A new approach is introduced that experimentally outperforms the currently most efficient technique.

Consensus-finding plays a ubiquitous role in A.I. In this paper, a consensus among agents is defined as a non-contradictory fragment of all the information conveyed by the agents such that this fragment does not logically conflict with any of the agents. This concept is investigated in modal logic S5 in order to meet representation needs that are put in light by this concept of consensus itself. Interestingly, an optimization-based approach to compute maximal consensuses is developed and shown experimentally efficient very often for both the standard Boolean and S5 frameworks.

An original method for the extraction of one maximal subset of a set of Boolean clauses that must be satisfiable with possibly mutually contradictory assumptive contexts is motivated and experimented. Noticeably, it performs a direct computation and avoids the enumeration of all subsets that are satisfiable with at least one of the contexts. The method applies for subsets that are maximal with respect to inclusion or cardinality.

The concepts of MSS (Maximal Satisfiable Subset) andCoMSS (also called Minimal Correction Subset) playa key role in many A.I. approaches and techniques. Inthis paper, a novel algorithm for partitioning a BooleanCNF formula into one MSS and the correspondingCoMSS is introduced. Extensive empirical evaluationshows that it is more robust and more efficient on mostinstances than currently available techniques.

A method is proposed to enforce specific solutions in constraint networks. Contrary to previous approaches, it yields a set of constraints to be dropped whose cardinality is minimal.

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.

An original encoding of multiple contraction in Boolean logic through Partial-Max-SAT is proposed. Multiple contraction of a set of clauses Δ by a set of formulas Γ delivers one maximum cardinality subset of Δ from which no formula of Γ can be deduced. Equivalently, multiple contraction can be defined as the extraction of one maximum cardinality subset of Δ that is satisfiable together with a given set of formulas. Noticeably, the encoding schema allows multiple contraction to be computed through a number of calls to a SAT solver that is bound by the number of formulas in Γ and one call to Partial-Max-SAT. On the contrary, in the worst case, a direct approach requires us to compute for each formula γ in Γ all inclusion-maximal subsets of Δ that do not entail γ. Extensive experimental results show that the encoding allows multiple contraction to be computed in a way that is practically viable in many cases and outperforms the direct approach.

Summary form only given. Belief change has long been a major topic of research in artificial intelligence, giving rise to very active subareas of their own, like belief revision, update and knowledge fusion. Much focus has been devoted to belief change in the situations where the incoming information in interaction with the previous available beliefs leads to logical inconsistency. When no logical conflict arises, the new information is just added to the current state of beliefs. On the contrary, we claim that many situations require some change in the pre-existing beliefs in front of an incoming piece of information, even when no logical conflict arises. We claim that the agenda of logic based belief change research should be concerned with these other human reasoning paradigms, too.

In this paper, we show that the E-SquarO puzzle, which is an extension of the popular SquarO game, is NP-complete. We propose a SAT encoding of E-SquarO and investigate its practical computational properties.

When a constraint network is unsatisfiable, it can be of prime importance to provide the network designer with a full-fledged explanation of what causes the absence of any solution to the network. In this respect, minimal unsatisfiable cores (in short, MUCs) form the basis for such an explanation. Efficient MUC extractors are often made of an initial incomplete minimization step that delivers an upper-approximation of a MUC, followed by a refinement step. The first step is assumed crucial for the performance of the whole approach. In this paper, its actual importance is investigated. Especially, it is shown that the first step can be skipped when the refinement process dynamically exploits the information that this latter treatment itself entails.

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.

This paper is concerned with a form of relaxation of constraint networks. The focus is on situations where additional constraints are intended to extend a non-empty set of preexisting solutions. These constraints require a specific treatment since merely inserting them inside the network would lead to their preemption by more restrictive ones. Several approaches to handle these additional constraints are investigated from conceptual and experimental points of view.

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.

These last years, the issue of locating and explaining contradictions inside sets of propositional clauses has received a renewed attention due to the emergence of very efficient SAT solvers. In case of inconsistency, many such solvers merely conclude that no solution exists or provide an upper approximation of the subset of clauses that are contradictory. However, in most application domains, only knowing that a problem does not admit any solution is not enough informative, and it is important to know which clauses are actually conflicting. In this paper, the focus is on the concept of Minimally Unsatisfiable Subformulas (MUSes), which explain logical inconsistency in terms of minimal sets of contradictory clauses. Specifically, various recent results and computational approaches about MUSes and related concepts are discussed.

In this paper, a new heuristic-based approach is introduced to extract minimally unsatisfiable subformulas (in short, MUSes) of SAT instances. It is shown that it often outperforms competing methods. Then, the focus is on inconsistent covers, which represent sets of MUSes that cover enough independent sources of infeasibility for the instance to regain satisfiability if they were repaired. As the number of MUSes can be exponential with respect to the size of the instance, it is shown that such a concept is often a viable trade-off since it does not require us to compute all MUSes but provides us with enough mutually independent infeasibility causes that need to be addressed in order to restore satisfiability

In the full paper, the problem of fusing various sources of legal knowledge is addressed. It is shown that standard logic-based approaches to knowledge fusion can unfortunately transform necessary conditions for a rule to apply into sufficient ones. A transformation schema that solves this problem is then proposed and analyzed.

Many approaches to handle inconsistent knowledge require some information to be dropped in order to ensure logical consistency. In this paper, a syntax-based technique that simply weakens the conflicting information by means of semaphores is proposed and analyzed in the context of the fusion of several possibly mutually conflicting knowledge sources. The proposed approach basically adopts a neutral position w.r.t. two knowledge sources in the sense that it does not conduct one source to predominate the other one. However marking a preference for one source and retracting this preference is easy. When the fusion process is iterated, it is shown that semaphores can conduct sources to become actually rejected. Conditions preventing such a drawback are investigated. It is also shown how this problem can be solved when all sources are available simultaneously and how a preference for less-contradicted sources can be realized as well.

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 problem of fusing logic-based technical specification knowledge components of a physical device or process, is investigated. It is shown that most standard logic approaches to beliefs fusion are not relevant in this context since some rules should be merged even in the case of a consistent fusion. Accordingly, we discuss the various types of formulas that should be merged during a fusion process, in order to avoid necessary conditions for the absence of failure to become sufficient conditions. This transformation is then described formally. It can be performed as an efficient preprocessing step on the knowledge components to be fused. The properties of this transformation schema are then investigated from a semantical point of view. Finally, a series of subsumption tests are proposed, preventing conditions of absence of failure from being overridden by subsumption.

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.

In this paper, a new efficient technique is introduced to check the logical consistency of finite first-order stratified KBs. It is based on a progressive instantiation schema that enables us to benefit from the power of local search techniques for propositional satisfiability and search. It combines a knowledge preference pre-ordering with a concept of depth-limited reasoning. An algorithm that proves to be efficient is proposed. It delivers a good approximation of (Benferhat et al., 1993) preferred maximal inclusion-based consistent sub-bases.

We propose a new computational approach to logic-based systems that should reason in a fast but logically sound and complete manner about large-scale complex critical devices and systems that can exhibit unexpected faulty behaviors. The approach is original from at least two points of view. First, it makes use of local search techniques while preserving logical deductive completeness. Second, it proves experimentally efficient for very large knowledge bases thanks to new heuristics in the use of local search techniques.

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.

In this paper, a notion of novelty of a formula for a concept w.r.t. a deductive database is investigated from a logical point of view. Intuitively, a formula is new for a concept when inserting the formula together with some additional information in the database allows us to infer an instance of the concept (or its negation) from the resulting database, while this proves impossible when only the additional information is inserted. First, this notion is analysed in the framework of first-order Herbrand monotonic databases. A decision procedure is provided, based on a prime implicants characterization. Then, novelty is investigated in the context of non-monotonic—completed—databases. Actually, four types of novelty are put forward to capture various intuitions about the relations between novelty and forms of non-monotonicity. These types of novelty are proved incomparable in the general case and their decision problems are discussed. Finally, possible applications of novelty in the database field are presented.