More than ever, air transport players (i.e., airline and airport companies) in an intensely competitive climate need to benefit from a carefully optimized management of airport resources to improve the quality of service and control the induced costs. In this paper, we investigate the Airport Check-in Desk Assignment Problem. We propose a Constraint Programming (CP) model for this problem, and present some promising experimental results from data coming from ADP (Aéroport de Paris). Our works are deployed in a preprod environment since 1 year.

Punctuality is a sensitive issue in large airports and hubs for passenger experience and for controlling operational costs. This paper presents a real and challenging problem of predicting and explaining flight off-block delays. We study the case of the international airport Paris Charles de Gaulle (Paris-CDG) starting from the specificities of this problem at Paris-CDG until the proposal of modelings then solutions and the analysis of the results on real data covering an entire year of activity. The proof of concept provided in this paper allows us to believe that the proposed approach could help improve the management of delays and reduce the impact of the resulting consequences.

International audience

International audience

The ever increasing complexity of machine learning techniques used more and more in practice, gives rise to the need to explain the outcomes of these models, often used as black-boxes. Explainable AI approaches are either numerical feature-based aiming to quantify the contribution of each feature in a prediction or symbolic providing certain forms of symbolic explanations such ascounterfactuals. This paper proposes a generic agnostic approach named ASTERYX allowing to generate both symbolic explanations and score-based ones. Our approach is declarative and it is based on the encoding of the model to be explained in an equivalent symbolic representation. This latter serves to generate in particular two types of symbolic explanations which aresufficient reasons andcounterfactuals. We then associate scores reflecting the relevance of the explanations and the features w.r.t to some properties. Our experimental results show the feasibility of the proposed approach and its effectiveness in providing symbolic and score-based explanations.

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.

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 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 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 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

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, 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.