Arrow Research search

Author name cluster

Jean-Marie Lagniez

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

54 papers
2 author rows

Possible papers

54

IJCAI Conference 2025 Conference Paper

Circuit-Aware d-DNNF Compilation

  • Vincent Derkinderen
  • Jean-Marie Lagniez

Boolean circuits in d-DNNF (determinstic Decomposable Negation Normal Form) enable tractable probabilistic inference, motivating research into compilers that transform arbitrary Boolean circuit into this form. However, d-DNNF compilers commonly require the input to be in conjunctive normal form (CNF), which means that a user must first convert their Boolean circuit into CNF. In this work, we argue that d-DNNF compilation would substantially benefit from reasoning over the original input circuit's structure, rather than solely relying on its CNF representation. To this end, we adapt an existing compiler and implement an optimisation that becomes more readily available once we reason over the input circuit: the identification and elimination of don't care variables. We empirically demonstrate the effectiveness of this approach, achieving a significant improvement in both the number of solved instances and the size of the resulting circuits.

PDF Details DOI

UAI Conference 2025 Conference Paper

Probabilistic Explanations for Regression Models

  • Frédéric Koriche
  • Jean-Marie Lagniez
  • Chi Tran

Formal explainability is an emerging field that aims to provide mathematically guaranteed explanations for the predictions made by machine learning models. Recent work in this area focuses on computing “probabilistic explanations” for the predictions made by classifiers based on specific data instances. The goal of this paper is to extend the concept of probabilistic explanations to the regression setting, treating the target regressor as a black box function. The class of probabilistic explanations consists of linear functions that meet a sparsity constraint, alongside a hyperplane constraint defined for the data instance being explained. While minimizing the precision error of such explanations is generally $\text{NP}^{\text{PP}}$-hard, we demonstrate that it can be approximated by substituting the precision measure with a fidelity measure. Optimal explanations based on this fidelity objective can be effectively approached using Mixed Integer Programming (MIP). Moreover, we show that for certain distributions used to define the precision measure, explanations with approximation guarantees can be computed in polynomial time using a variant of Iterative Hard Thresholding (IHT). Experiments conducted on various datasets indicate that both the MIP and IHT approaches outperform the state-of-the-art LIME and MAPLE explainers.

Details

AAMAS Conference 2024 Conference Paper

A SAT-based Approach for Argumentation Dynamics

  • Jean-Marie Lagniez
  • Emmanuel Lonca
  • Jean-Guy Mailly

In the realm of multi-agent systems, argumentative dialogues for persuasion and negotiation involve autonomous agents exchanging arguments, necessitating continual re-evaluation of argument acceptability. This study introduces a novel approach using modern SAT solving techniques to dynamically reassess the acceptability status of arguments, aligning with various classical semantics. Our method uses the assumption mechanism in SAT solvers, distinguished by minimal assumptions, ensuring practicality.

PDF

IJCAI Conference 2024 Conference Paper

A Top-Down Tree Model Counter for Quantified Boolean Formulas

  • Florent Capelli
  • Jean-Marie Lagniez
  • Andreas Plank
  • Martina Seidl

This paper addresses the challenge of solution counting for Quantified Boolean Formulas (QBFs), a task distinct from the well-established model counting problem for SAT (\#SAT). Unlike SAT, where models are straightforward assignments to Boolean variables, QBF solution counting involves tree models that capture dependencies among variables within different quantifier blocks. We present a comprehensive top-down tree model counter capable of handling diverse satisfiable QBF formulas. Emphasizing the critical role of the branching heuristic, which must consider variables in the correct order according to quantification blocks, we further demonstrate the importance of addressing connected components, free variables, and caching. Experimental results indicate that our proposed approach for counting tree models of QBF formulas is highly efficient in practice, surpassing existing state-of-the-art methods designed for this specific purpose.

PDF Details DOI

IJCAI Conference 2024 Conference Paper

Deriving Provably Correct Explanations for Decision Trees: The Impact of Domain Theories

  • Gilles Audemard
  • Jean-Marie Lagniez
  • Pierre Marquis
  • Nicolas Szczepanski

We are interested in identifying the complexity of computing local explanations of various types given a decision tree, when the Boolean conditions used in the tree are not independent. This is usually the case when decision trees are learned from instances described using numerical or categorical attributes. In such a case, considering the domain theory indicating how the Boolean conditions occurring in the tree are logically connected is paramount to derive provably correct explanations. However, the nature of the domain theory may have a strong impact on the complexity of generating explanations. In this paper, we identify the complexity of deriving local explanations (abductive or contrastive) given a decision tree in the general case, and under several natural restrictions about the domain theory.

PDF Details DOI

SAT Conference 2024 Conference Paper

Dynamic Blocked Clause Elimination for Projected Model Counting

  • Jean-Marie Lagniez
  • Pierre Marquis
  • Armin Biere

In this paper, we explore the application of blocked clause elimination for projected model counting. This is the problem of determining the number of models ‖∃ X. Σ‖ of a propositional formula Σ after eliminating a given set X of variables existentially. Although blocked clause elimination is a well-known technique for SAT solving, its direct application to model counting is challenging as in general it changes the number of models. However, we demonstrate, by focusing on projected variables during the blocked clause search, that blocked clause elimination can be leveraged while preserving the correct model count. To take advantage of blocked clause elimination in an efficient way during model counting, a novel data structure and associated algorithms are introduced. Our proposed approach is implemented in the model counter d4. Our experiments demonstrate the computational benefits of our new method of blocked clause elimination for projected model counting.

Details

KR Conference 2024 Conference Paper

Leveraging Decision-DNNF Compilation for Enumerating Disjoint Partial Models

  • Jean-Marie Lagniez
  • Emmanuel Lonca

The All-Solution Satisfiability Problem (AllSAT) extends SAT by requiring the identification of all possible solutions for a propositional formula. In practice, enumerating all complete models is often infeasible, making the identification of partial models essential for generating a concise representation of the solution set. Deterministic Decomposable Negation Normal Form (d-DNNF) serves as a language for representation known to offer polynomial-time algorithms for model enumeration. Specifically, when a propositional formula is encoded in d-DNNF, it enables iterative model enumeration with polynomial delay between models. However, despite the existence of theoretical algorithms for this purpose, no available implementations are currently accessible. Furthermore, these theoretical approaches are nearly impractical as they solely yield complete models. We introduce a novel algorithm that maintains a polynomial delay between partial models while significantly enhancing efficiency compared to baseline approaches. Furthermore, through experimental validation, we demonstrate the superiority of compiling a CNF formula Σ into a d-DNNF formula Σ′ and subsequently enumerating models of Σ′ over existing state-of-the-art methodologies for CNF partial model enumeration.

PDF Details DOI

ECAI Conference 2024 Conference Paper

On the Computation of Contrastive Explanations for Boosted Regression Trees

  • Gilles Audemard
  • Jean-Marie Lagniez
  • Pierre Marquis

A contrastive explanation is a local explanation that is looked for when the prediction achieved by an ML model on an input instance x differs from what was foreseen. A contrastive explanation indicates how to change x to another instance xc from which a prediction that complies with the user’s expectations can be obtained. In this paper, we present a constraint-based approach to the generation of contrastive explanations that are suited to regression functions represented by boosted trees. We show how to compute the smallest interval containing all the regression values that are attainable given a set of characteristics of x that are protected (i. e. , not amenable to change). We also show how to generate minimal contrastive explanations for x given a target interval, i. e. , instances with regression values within the specified interval and that are as close as possible to x. Closeness is captured using user-dependent mappings reflecting preferences about value change for the attributes (or combinations of attributes) considered in the representation of x.

Details

IJCAI Conference 2024 Conference Paper

On the Computation of Example-Based Abductive Explanations for Random Forests

  • Gilles Audemard
  • Jean-Marie Lagniez
  • Pierre Marquis
  • Nicolas Szczepanski

We show how to define and compute example-based abductive explanations. Such explanations are guaranteed to be 100% correct, fairly general, and persuasive enough since they cover sufficiently many reference instances furnished by the explainee. We prove that the latter coverage condition yields a complexity shift to the second level of the polynomial hierarchy. We present a CEGAR-based algorithm to derive such explanations, and show how to modify it to derive most anchored example-based abductive explanations, i. e. , example-based abductive explanations that cover as many reference instances as possible. We also explain how to reduce example-based abductive explanations to get subset-minimal explanations. Experiments in the case of random forest classifiers show that our CEGAR-based algorithm is quite efficient in practice.

PDF Details DOI

IJCAI Conference 2024 Conference Paper

PyXAI: An XAI Library for Tree-Based Models

  • Gilles Audemard
  • Jean-Marie Lagniez
  • Pierre Marquis
  • Nicolas Szczepanski

PyXAI (Python eXplainable AI) is a Python library designed for providing explanations and cor- recting tree-based Machine Learning (ML) models. It is suited to decision trees, random forests, and boosted trees, when used for regression or classification tasks. In contrast to many model-agnostic approaches to XAI, PyXAI exploits the model it- self to generate explanations, ensuring them to be faithful. PyXAI includes several algorithms for the generation of explanations, which can be abductive or contrastive. PyXAI also includes algorithms for correcting tree-based models when their predictions conflict with pieces of user knowledge.

PDF Details DOI

JAAMAS Journal 2023 Journal Article

Algorithms for partially robust team formation

  • Nicolas Schwind
  • Emir Demirović
  • Jean-Marie Lagniez

Abstract In one of its simplest forms, Team Formation involves deploying the least expensive team of agents while covering a set of skills. While current algorithms are reasonably successful in computing the best teams, the resilience to change of such solutions remains an important concern: Once a team has been formed, some of the agents considered at start may be finally defective and some skills may become uncovered. Two recently introduced solution concepts deal with this issue proactively: 1) form a team which is robust to changes so that after some agent losses, all skills remain covered, and 2) opt for a recoverable team, i. e. , it can be "repaired" in the worst case by hiring new agents while keeping the overall deployment cost minimal. In this paper, we introduce the problem of partially robust team formation (PR–TF). Partial robustness is a weaker form of robustness which guarantees a certain degree of skill coverage after some agents are lost. We analyze the computational complexity of PR-TF and provide two complete algorithms for it. We compare the performance of our algorithms with the existing methods for robust and recoverable team formation on several existing and newly introduced benchmarks. Our empirical study demonstrates that partial robustness offers an interesting trade-off between (full) robustness and recoverability in terms of computational efficiency, skill coverage guaranteed after agent losses and repairability. This paper is an extended and revised version of as reported by (Schwind et al. , Proceedings of the 20th International Conference on Autonomous Agents and Multiagent Systems (AAMAS’21), pp. 1154–1162, 2021).

Details DOI

JELIA Conference 2023 Conference Paper

Boosting Definability Bipartition Computation Using SAT Witnesses

  • Jean-Marie Lagniez
  • Pierre Marquis

Abstract Bipartitioning the set of variables \( Var (\varSigma )\) of a propositional formula \(\varSigma \) w. r. t. definability consists in pointing out a bipartition \(\langle I, O\rangle \) of \( Var (\varSigma )\) such that \(\varSigma \) defines the variables of O (outputs) in terms of the variables in I (inputs), i. e. , for every \(o \in O\), there exists a formula \(\varPhi _o\) over I such that \(o \Leftrightarrow \varPhi _o\) is a logical consequence of \(\varSigma \). The existence of \(\varPhi _o\) given o, I, and \(\varSigma \) is a coNP -complete problem, and as such, it can be addressed in practice using a SAT solver. From a computational perspective, definability bipartitioning has been shown as a valuable preprocessing technique for model counting, a key task for a number of AI problems involving probabilities. To maximize the benefits offered by such a preprocessing, one is interested in deriving subset-minimal bipartitions in terms of input variables, i. e. , definability bipartitions \(\langle I, O\rangle \) such that for every \(i \in I\), \(\langle I \setminus \{i\}, O \cup \{i\}\rangle \) is not a definability bipartition. We show how the computation of subset-minimal bipartitions can be boosted by leveraging not only the decisions furnished by SAT solvers (as done in previous approaches), but also the SAT witnesses (models and cores) justifying those decisions.

Details

IJCAI Conference 2023 Conference Paper

Computing Abductive Explanations for Boosted Regression Trees

  • Gilles Audemard
  • Steve Bellart
  • Jean-Marie Lagniez
  • Pierre Marquis

We present two algorithms for generating (resp. evaluating) abductive explanations for boosted regression trees. Given an instance x and an interval I containing its value F (x) for the boosted regression tree F at hand, the generation algorithm returns a (most general) term t over the Boolean conditions in F such that every instance x′ satisfying t is such that F (x′ ) ∈ I. The evaluation algorithm tackles the corresponding inverse problem: given F, x and a term t over the Boolean conditions in F such that t covers x, find the least interval I_t such that for every instance x′ covered by t we have F (x′ ) ∈ I_t. Experiments on various datasets show that the two algorithms are practical enough to be used for generating (resp. evaluating) abductive explanations for boosted regression trees based on a large number of Boolean conditions.

PDF Details DOI

ECAI Conference 2023 Conference Paper

On Contrastive Explanations for Tree-Based Classifiers

  • Gilles Audemard
  • Jean-Marie Lagniez
  • Pierre Marquis
  • Nicolas Szczepanski

We define contrastive explanations that are suited to tree-based classifiers. In our framework, contrastive explanations are based on the set of (possibly non-independent) Boolean characteristics used by the classifier and are at least as general as contrastive explanations based on the set of characteristics of the instances considered at start. We investigate the computational complexity of computing contrastive explanations for Boolean classifiers (including tree-based ones), when the Boolean conditions used are not independent. Finally, we present and evaluate empirically an algorithm for computing minimum-size contrastive explanations for random forests.

Details

SAT Conference 2022 Conference Paper

A New Exact Solver for (Weighted) Max#SAT

  • Gilles Audemard
  • Jean-Marie Lagniez
  • Marie Miceli

We present and evaluate d4Max, an exact approach for solving the Weighted Max#SAT problem. The Max#SAT problem extends the model counting problem (#SAT) by considering a tripartition of the variables {X, Y, Z}, and consists in maximizing over X the number of assignments to Y that can be extended to a solution with some assignment to Z. The Weighted Max#SAT problem is an extension of the Max#SAT problem with weights associated on each interpretation. We test and compare our approach with other state-of-the-art solvers on the challenging task in probabilistic inference of finding the marginal maximum a posteriori probability (MMAP) of a given subset of the variables in a Bayesian network and on exist-random quantified SSAT benchmarks. The results clearly show the overall superiority of d4Max in term of speed and number of instances solved. Moreover, we experimentally show that, in general, d4Max is able to quickly spot a solution that is close to optimal, thereby opening the door to an efficient anytime approach.

Details

IJCAI Conference 2022 Conference Paper

On Preferred Abductive Explanations for Decision Trees and Random Forests

  • Gilles Audemard
  • Steve Bellart
  • Louenas Bounia
  • Frederic Koriche
  • Jean-Marie Lagniez
  • Pierre Marquis

Abductive explanations take a central place in eXplainable Artificial Intelligence (XAI) by clarifying with few features the way data instances are classified. However, instances may have exponentially many minimum-size abductive explanations, and this source of complexity holds even for ``intelligible'' classifiers, such as decision trees. When the number of such abductive explanations is huge, computing one of them, only, is often not informative enough. Especially, better explanations than the one that is derived may exist. As a way to circumvent this issue, we propose to leverage a model of the explainee, making precise her / his preferences about explanations, and to compute only preferred explanations. In this paper, several models are pointed out and discussed. For each model, we present and evaluate an algorithm for computing preferred majoritary reasons, where majoritary reasons are specific abductive explanations suited to random forests. We show that in practice the preferred majoritary reasons for an instance can be far less numerous than its majoritary reasons.

PDF Details DOI

AAAI Conference 2022 Conference Paper

Trading Complexity for Sparsity in Random Forest Explanations

  • Gilles Audemard
  • Steve Bellart
  • Louènas Bounia
  • Frédéric Koriche
  • Jean-Marie Lagniez
  • Pierre Marquis

Random forests have long been considered as powerful model ensembles in machine learning. By training multiple decision trees, whose diversity is fostered through data and feature subsampling, the resulting random forest can lead to more stable and reliable predictions than a single decision tree. This however comes at the cost of decreased interpretability: while decision trees are often easily interpretable, the predictions made by random forests are much more difficult to understand, as they involve a majority vote over multiple decision trees. In this paper, we examine different types of reasons that explain “why” an input instance is classified as positive or negative by a Boolean random forest. Notably, as an alternative to prime-implicant explanations taking the form of subset-minimal implicants of the random forest, we introduce majoritary reasons which are subset-minimal implicants of a strict majority of decision trees. For these abductive explanations, the tractability of the generation problem (finding one reason) and the optimization problem (finding one minimumsized reason) are investigated. Unlike prime-implicant explanations, majoritary reasons may contain redundant features. However, in practice, prime-implicant explanations for which the identification problem is DP-complete - are slightly larger than majoritary reasons that can be generated using a simple linear-time greedy algorithm. They are also significantly larger than minimum-sized majoritary reasons which can be approached using an anytime PARTIAL MAXSAT algorithm.

PDF Details

AAAI Conference 2021 Conference Paper

Certifying Top-Down Decision-DNNF Compilers

  • Florent Capelli
  • Jean-Marie Lagniez
  • Pierre Marquis

Certifying the output of tools solving complex problems so as to ensure the correctness of the results they provide is of tremendous importance. Despite being widespread for SATsolvers, this level of exigence has not yet percolated for tools solving more complex tasks, such as model counting or knowledge compilation. In this paper, the focus is laid on a general family of top-down Decision-DNNF compilers. We explain how those compilers can be tweaked so as to output certifiable Decision-DNNF circuits, which are mainly standard Decision-DNNF circuits decorated by annotations serving as certificates. We describe a polynomial-time checker for testing whether a given CNF formula is equivalent or not to a given certifiable Decision-DNNF circuit. Finally, leveraging a modified version of the compiler D4 for generating certifiable Decision-DNNF circuits and an implementation of the checker, we present the results of an empirical evaluation that has been conducted for assessing how large are the certifiable Decision-DNNF circuits that can be generated in practice, and how much time is needed to compute and to check such circuits.

PDF Details

KR Conference 2021 Conference Paper

On the Computational Intelligibility of Boolean Classifiers

  • Gilles Audemard
  • Steve Bellart
  • Louenas Bounia
  • Frédéric Koriche
  • Jean-Marie Lagniez
  • Pierre Marquis

In this paper, we investigate the computational intelligibility of Boolean classifiers, characterized by their ability to answer XAI queries in polynomial time. The classifiers under consideration are decision trees, DNF formulae, decision lists, decision rules, tree ensembles, and Boolean neural nets. Using 9 XAI queries, including both explanation queries and verification queries, we show the existence of large intelligibility gap between the families of classifiers. On the one hand, all the 9 XAI queries are tractable for decision trees. On the other hand, none of them is tractable for DNF formulae, decision lists, random forests, boosted decision trees, Boolean multilayer perceptrons, and binarized neural networks.

PDF Details DOI

AAMAS Conference 2021 Conference Paper

Partial Robustness in Team Formation: Bridging the Gap between Robustness and Resilience

  • Nicolas Schwind
  • Emir Demirović
  • Katsumi Inoue
  • Jean-Marie Lagniez

Team formation is the problem of deploying the least expensive team of agents while covering a set of skills. Once a team has been formed, some of the agents considered at start may be finally defective and some skills may become uncovered. Two solution concepts have been recently introduced to deal with this issue in a proactive manner: one may form a team which is robust to changes so that after some agent losses, all skills remain covered; or one may opt for a recoverable team, i. e. , it can be “repaired” in the worst case by hiring new agents while keeping the overall deployment cost minimal. In this paper, we introduce the problem of partially robust team formation (PR-TF). Partial robustness is a weaker form of robustness which guarantees a certain degree of skill coverage after some agents are lost. We analyze the computational complexity of PR-TF, and provide a complete algorithm for it. The performance of our algorithm is empirically compared with the existing methods for robust and recoverable team formation, on a number of existing benchmarks and some newly introduced ones. Partial robustness is shown to be an interesting trade-off notion between (full) robustness and recoverability in terms of computational efficiency, skill coverage guarantees after agent losses, and repairability.

PDF

ECAI Conference 2020 Conference Paper

Consolidating Modal Knowledge Bases

  • Zied Bouraoui
  • Jean-Marie Lagniez
  • Pierre Marquis
  • Valentin Montmirail

This paper introduces a novel approach to the consolidation of knowledge bases represented as modal logic formulae. The objective is to turn the given knowledge base into another knowledge base such that the latter is consistent even when the former is not. Our approach follows a strategy that locally spots and iteratively consolidates inconsistent subformulae of the input knowledge base. Existing methods for consolidating a knowledge base typically consist in selecting some of its maximal consistent subbases. Such methods are suited to the case the input is a (conjunctively-interpreted) set of formulae. However, they are inadequate when the input consists of a single inconsistent modal formula since, in the modal case, a formula cannot always be turned into a conjunction of simpler formulae. Furthermore, such methods consolidate any base consisting of a single inconsistent formula into the empty base. Our approach does not suffer from such limitations and preserves more information in the general case. From a computational point of view, it ensures that the size of the consolidated base is bounded by the size of the input knowledge base. We present some empirical results demonstrating the practical feasibility of our approach.

Details

AIJ Journal 2020 Journal Article

Definability for model counting

  • Jean-Marie Lagniez
  • Emmanuel Lonca
  • Pierre Marquis

We define and evaluate a new preprocessing technique for propositional model counting. This technique leverages definability, i. e. , the ability to determine that some gates are implied by the input formula Σ. Such gates can be exploited to simplify Σ without modifying its number of models. Unlike previous techniques based on gate detection and replacement, gates do not need to be made explicit in our approach. Our preprocessing technique thus consists of two phases: computing a bipartition 〈 I, O 〉 of the variables of Σ where the variables from O are defined in Σ in terms of I, then eliminating some variables of O in Σ. Our experiments show the computational benefits which can be achieved by taking advantage of our preprocessing technique for model counting.

Details DOI

LPAR Conference 2020 Conference Paper

NACRE - A Nogood And Clause Reasoning Engine

  • Gael Glorian
  • Jean-Marie Lagniez
  • Christophe Lecoutre

NACRE, for Nogood And Clause Reasoning Engine, is a constraint solver written in C++. It is based on a modular architecture designed to work with generic constraints while implementing several state-of-the-art search methods and heuristics. Interestingly, its data structures have been carefully designed to play around nogoods and clauses, making it suit- able for implementing learning strategies. NACRE was submitted to the CSP MiniTrack of the 2018 and 2019 XCSP3 [8] competitions where it took the first place. This paper gives a general description of NACRE as a framework. We present its kernel, the available search algorithms, and the default settings (notably, used for XCSP3 competitions), which makes NACRE efficient in practice when used as a black-box solver.

Details

IJCAI Conference 2020 Conference Paper

On Computational Aspects of Iterated Belief Change

  • Nicolas Schwind
  • Sebastien Konieczny
  • Jean-Marie Lagniez
  • Pierre Marquis

Iterated belief change aims to determine how the belief state of a rational agent evolves given a sequence of change formulae. Several families of iterated belief change operators (revision operators, improvement operators) have been pointed out so far, and characterized from an axiomatic point of view. This paper focuses on the inference problem for iterated belief change, when belief states are represented as a special kind of stratified belief bases. The computational complexity of the inference problem is identified and shown to be identical for all revision operators satisfying Darwiche and Pearl's (R*1-R*6) postulates. In addition, some complexity bounds for the inference problem are provided for the family of soft improvement operators. We also show that a revised belief state can be computed in a reasonable time for large-sized instances using SAT-based algorithms, and we report empirical results showing the feasibility of iterated belief change for bases of significant sizes.

PDF Details DOI

AAAI Conference 2019 Conference Paper

A Recursive Algorithm for Projected Model Counting

  • Jean-Marie Lagniez
  • Pierre Marquis

We present a recursive algorithm for projected model counting, i. e. , the problem consisting in determining the number of models k∃X. Σk of a propositional formula Σ after eliminating from it a given set X of variables. Based on a ”standard” model counter, our algorithm projMC takes advantage of a disjunctive decomposition scheme of ∃X. Σ for computing k∃X. Σk. It also looks for disjoint components in its input for improving the computation. Our experiments show that in many cases projMC is significantly more efficient than the previous algorithms for projected model counting from the literature.

PDF Details

IJCAI Conference 2019 Conference Paper

What Has Been Said? Identifying the Change Formula in a Belief Revision Scenario

  • Nicolas Schwind
  • Katsumi Inoue
  • Sébastien Konieczny
  • Jean-Marie Lagniez
  • Pierre Marquis

We consider the problem of identifying the change formula in a belief revision scenario: given that an unknown announcement (a formula mu) led a set of agents to revise their beliefs and given the prior beliefs and the revised beliefs of the agents, what can be said about mu? We show that under weak conditions about the rationality of the revision operators used by the agents, the set of candidate formulae has the form of a logical interval. We explain how the bounds of this interval can be tightened when the revision operators used by the agents are known and/or when mu is known to be independent from a given set of variables. We also investigate the completeness issue, i. e. , whether mu can be exactly identified. We present some sufficient conditions for it, identify its computational complexity, and report the results of some experiments about it.

PDF Details

IJCAI Conference 2018 Conference Paper

Boosting MCSes Enumeration

  • Éric Grégoire
  • Yacine Izza
  • Jean-Marie Lagniez

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.

PDF Details

IJCAI Conference 2018 Conference Paper

DMC: A Distributed Model Counter

  • Jean-Marie Lagniez
  • Pierre Marquis
  • Nicolas Szczepanski

We present and evaluate DMC, a distributed model counter for propositional CNF formulae based on the state-of-the-art sequential model counter D4. DMC can take advantage of a (possibly large) number of sequential model counters running on (possibly heterogeneous) computing units spread over a network of computers. For ensuring an efficient workload distribution, the model counting task is shared between the model counters following a policy close to work stealing. The number and the sizes of the messages which are exchanged by the jobs are kept small. The results obtained show DMC as a much more efficient counter than D4, the distribution of the computation yielding large improvements for some benchmarks. DMC appears also as a serious challenger to the parallel model counter CountAntom and to the distributed model counter dCountAntom.

PDF Details

KR Conference 2018 Short Paper

Probabilistic Coalition Structure Generation

  • Nicolas Schwind
  • Tenda Okimoto
  • Katsumi Inoue
  • Katsutoshi Hirayama
  • Jean-Marie Lagniez
  • Pierre Marquis

F (CS) = Ci ∈CS f (Ci). A coalition structure CS ∈ ΠA We introduce a model for probabilistic coalition structure generation (PCSG). This model generalizes the standard CSG model to the case when some of the agents considered at start may be finally defective but a new coalition structure based on the remaining agents cannot be formed. In a PCSG, one seeks to maximize the expected utility of a coalition structure. Two policies making precise how the value of a coalition structure evolves when some agents are missing are also introduced.

SAT Conference 2017 Conference Paper

A Distributed Version of Syrup

  • Gilles Audemard
  • Jean-Marie Lagniez
  • Nicolas Szczepanski
  • Sébastien Tabary

Abstract A portfolio SAT solver has to share clauses in order to be efficient. In a distributed environment, such sharing implies additional problems: more information has to be exchanged and communications among solvers can be time consuming. In this paper, we propose a new version of the state-of-the-art SAT solver Syrup that is now able to run on distributed architectures. We analyze and compare different programming models of communication. We show that, using a dedicated approach, it is possible to share many clauses without penalizing the solvers. Experiments conducted on SAT 2016 benchmarks with up to 256 cores show that our solver is very effective and outperforms other approaches. This opens a broad range of possibilities to boost parallel solvers needing to share many data.

Details

IJCAI Conference 2017 Conference Paper

A Recursive Shortcut for CEGAR: Application To The Modal Logic K Satisfiability Problem

  • Jean-Marie Lagniez
  • Daniel Le Berre
  • Tiago de Lima
  • Valentin Montmirail

Counter-Example-Guided Abstraction Refinement (CEGAR) has been very successful in model checking large systems. Since then, it has been applied to many different problems. It especially proved to be an highly successful practical approach for solving the PSPACE complete QBF problem. In this paper, we propose a new CEGAR-like approach for tackling PSPACE complete problems that we call RECAR (Recursive Explore and Check Abstraction Refinement). We show that this generic approach is sound and complete. Then we propose a specific implementation of the RECAR approach to solve the modal logic K satisfiability problem. We implemented both a CEGAR and a RECAR approach for the modal logic K satisfiability problem within the solver MoSaiC. We compared experimentally those approaches to the state-of-the-art solvers for that problem. The RECAR approach outperforms the CEGAR one for that problem and also compares favorably against the state-of-the-art on the benchmarks considered.

PDF Details

AAAI Conference 2017 Conference Paper

A SAT-Based Approach for Solving the Modal Logic S5-Satisfiability Problem

  • Thomas Caridroit
  • Jean-Marie Lagniez
  • Daniel Le Berre
  • Tiago de Lima
  • Valentin Montmirail

We present a SAT-based approach for solving the modal logic S5-satisfiability problem. That problem being NP-complete, the translation into SAT is not a surprise. Our contribution is to greatly reduce the number of propositional variables and clauses required to encode the problem. We first present a syntactic property called diamond degree. We show that the size of an S5-model satisfying a formula φ can be bounded by its diamond degree. Such measure can thus be used as an upper bound for generating a SAT encoding for the S5satisfiability of that formula. We also propose a lightweight caching system which allows us to further reduce the size of the propositional formula. We implemented a generic SATbased approach within the modal logic S5 solver S52SAT. It allowed us to compare experimentally our new upper-bound against previously known one, i. e. the number of modalities of φ and to evaluate the effect of our caching technique. We also compared our solver against existing modal logic S5 solvers. The proposed approach outperforms previous ones on the benchmarks used. These promising results open interesting research directions for the practical resolution of others modal logics (e. g. K, KT, S4)

PDF Details

IJCAI Conference 2017 Conference Paper

An Improved Decision-DNNF Compiler

  • Jean-Marie Lagniez
  • Pierre Marquis

We present and evaluate a new compiler, called d4, targeting the Decision-DNNF language. As the state-of-the-art compilers C2D and Dsharp targeting the same language, d4 is a top-down tree-search algorithm exploring the space of propositional interpretations. d4 is based on the same ingredients as those considered in C2D and Dsharp (mainly, disjoint component analysis, conflict analysis and non-chronological backtracking, component caching). d4 takes advantage of a dynamic decomposition approach based on hypergraph partitioning, used sparingly. Some simplification rules are also used to minimize the time spent in the partitioning steps and to promote the quality of the decompositions. Experiments show that the compilation times and the sizes of the Decision-DNNF representations computed by d4 are in many cases significantly lower than the ones obtained by C2D and Dsharp.

PDF Details

LORI Conference 2017 Conference Paper

Boosting Distance-Based Revision Using SAT Encodings

  • Sébastien Konieczny
  • Jean-Marie Lagniez
  • Pierre Marquis

Abstract Belief revision has been studied for more than 30 years, and the theoretical properties of the belief revision operators are now well-known. Contrastingly, there are almost no practical applications of these operators. One of the reasons is the computational complexity of the corresponding inference problem, which is typically NP -hard and coNP -hard. Especially, existing implementations of belief revision operators are capable to solve toy instances, but are still unable to cope with real-size problem instances. However, the improvements achieved by SAT solvers for the past few years have been very impressive and they allow to tackle the solving of instances of inference problems located beyond NP. In this paper we describe and evaluate SAT encodings for a large family of distance-based belief revision operators. The results obtained pave the way for the practical use of belief revision operators in large-scale applications.

Details

AAAI Conference 2017 Conference Paper

SAT Encodings for Distance-Based Belief Merging Operators

  • SŽbastien Konieczny
  • Jean-Marie Lagniez
  • Pierre Marquis

We present SAT encoding schemes for distance-based belief merging operators relying on the (possibly weighted) drastic distance or the Hamming distance between interpretations, and using sum, GMax (leximax) or GMin (leximin) as aggregation function. In order to evaluate these encoding schemes, we generated benchmarks of a time-tabling problem and translated them into belief merging instances. Then, taking advantage of these schemes, we compiled the merged bases of the resulting instances into query-equivalent CNF formulae. Experiments have shown the benefits which can be gained by considering the SAT encoding schemes we pointed out. Especially, thanks to them, we succeeded in computing query-equivalent formulae for merging instances based on hundreds of variables, which are out of reach of previous implementations.

PDF Details

ECAI Conference 2016 Conference Paper

A Computational Approach to Consensus-Finding

  • Éric Grégoire
  • Jean-Marie Lagniez

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.

Details

ECAI Conference 2016 Conference Paper

An Improved CNF Encoding Scheme for Probabilistic Inference

  • Anicet Bart
  • Frédéric Koriche
  • Jean-Marie Lagniez
  • Pierre Marquis

We present and evaluate a new CNF encoding scheme for reducing probabilistic inference from a graphical model to weighted model counting. This new encoding scheme elaborates on the CNF encoding scheme ENC4 introduced by Chavira and Darwiche, and improves it by taking advantage of log encodings of the elementary variable/value assignments and of the implicit encoding of the most frequent probability value per conditional probability table. From the theory side, we show that our encoding scheme is faithful, and that for each input network, the CNF formula it leads to contains less variables and less clauses than the CNF formula obtained using ENC4. From the practical side, we show that the C2D compiler empowered by our encoding scheme performs in many cases significantly better than when ENC4 is used, or when the state-of-the-art ACE compiler is considered instead.

Details

IJCAI Conference 2016 Conference Paper

Improving Model Counting by Leveraging Definability

  • Jean-Marie Lagniez
  • Emmanuel Lonca
  • Pierre Marquis

We present a new preprocessing technique for propositional model counting. This technique leverages definability, i. e. , the ability to determine that some gates are implied by the input formula Σ . Such gates can be exploited to simplify Σ without modifying its number of models. Unlike previous techniques based on gate detection and replacement, gates do not need to be made explicit in our approach. Our preprocessing technique thus consists of two phases: computing a bipartition I, O of the variables of Σ where the variables from O are defined in Σ in terms of I, then eliminating some variables of O in Σ . Our experiments show the computational benefits which can be achieved by taking advantage of our preprocessing technique for model counting.

PDF Details

AAAI Conference 2016 Conference Paper

On the Extraction of One Maximal Information Subset That Does Not Conflict with Multiple Contexts

  • Éric Grégoire
  • Yacine Izza
  • Jean-Marie Lagniez

The efficient extraction of one maximal information subset that does not conflict with multiple contexts 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.

PDF Details

IJCAI Conference 2015 Conference Paper

Compiling Constraint Networks into Multivalued Decomposable Decision Graphs

  • Fr
  • eacute; d
  • eacute; ric Koriche
  • Jean-Marie Lagniez
  • Pierre Marquis
  • Samuel Thomas

We present and evaluate a top-down algorithm for compiling finite-domain constraint networks (CNs) into the language MDDG of multivalued decomposable decision graphs. Though it includes Decision- DNNF as a proper subset, MDDG offers the same key tractable queries and transformations as Decision- DNNF, which makes it useful for many applications. Intensive experiments showed that our compiler cn2mddg succeeds in compiling CNs which are out of the reach of standard approaches based on a translation of the input network to CNF, followed by a compilation to Decision-DNNF. Furthermore, the sizes of the resulting compiled representations turn out to be much smaller (sometimes by several orders of magnitude).

PDF Details

LPAR Conference 2015 Conference Paper

On Anti-subsumptive Knowledge Enforcement

  • Éric Grégoire
  • Jean-Marie Lagniez

Abstract The anti-subsumptive enforcement of a clause \(\delta \) in a set of clauses \(\varDelta \) consists in extracting one cardinality-maximal satisfiable subset \(\varDelta '\) of \(\varDelta \cup \{\delta \}\) that contains \(\delta \) but that does not strictly subsume \(\delta \). In this paper, the computational issues of this problem are investigated in the Boolean framework. Especially, the minimal change policy that requires a minimal number of clauses to be dropped from \(\varDelta \) can lead to an exponential computational blow-up. Indeed, a direct and natural approach to anti-subsumptive enforcement requires the computation of all inclusion-maximal subsets of \(\varDelta \cup \{\delta \}\) that, at the same time, contain \(\delta \) and are satisfiable with \(\lnot \delta _j\) where \(\delta _j\) is some strict sub-clause of \(\delta \). On the contrary, we propose a method that avoids the computation of this possibly exponential number of subsets of clauses. Interestingly, it requires only one single call to a Partial-Max-SAT procedure and appears tractable in many realistic situations, even for very large \(\varDelta \). Moreover, the approach is easily extended to take into account a preference pre-ordering between formulas and lay the foundations for the practical enumeration of all optimal solutions to the problem of making \(\delta \) subsumption-free in \(\varDelta \) under a minimal change policy.

Details

AAAI Conference 2015 Conference Paper

On Computing Maximal Subsets of Clauses that Must Be Satisfiable with Possibly Mutually-Contradictory Assumptive Contexts

  • Philippe Besnard
  • Eric Grégoire
  • Jean-Marie Lagniez

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.

PDF Details

AAAI Conference 2014 Conference Paper

An Experimentally Efficient Method for (MSS,CoMSS) Partitioning

  • Eric Grégoire
  • Jean-Marie Lagniez
  • Bertrand Mazure

The concepts of MSS (Maximal Satisfiable Subset) and CoMSS (also called Minimal Correction Subset) play a key role in many A. I. approaches and techniques. In this paper, a novel algorithm for partitioning a Boolean CNF formula into one MSS and the corresponding CoMSS is introduced. Extensive empirical evaluation shows that it is more robust and more efficient on most instances than currently available techniques.

PDF Details

ECAI Conference 2014 Conference Paper

Enforcing Solutions in Constraint Networks

  • Éric Grégoire
  • Jean-Marie Lagniez
  • Bertrand Mazure

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.

Details

AAAI Conference 2014 Conference Paper

Preprocessing for Propositional Model Counting

  • Jean-Marie Lagniez
  • Pierre Marquis

This paper is concerned with preprocessing techniques for propositional model counting. We have implemented a preprocessor which includes many elementary preprocessing techniques, including occurrence reduction, vivification, backbone identification, as well as equivalence, AND and XOR gate identification and replacement. We performed intensive experiments, using a huge number of benchmarks coming from a large number of families. Two approaches to model counting have been considered downstream: ”direct” model counting using Cachet and compilation-based model counting, based on the C2D compiler. The experimental results we have obtained show that our preprocessor is both efficient and robust.

PDF Details

ECAI Conference 2014 Conference Paper

Symmetry-Driven Decision Diagrams for Knowledge Compilation

  • Anicet Bart
  • Frédéric Koriche
  • Jean-Marie Lagniez
  • Pierre Marquis

In this paper, symmetries are exploited for achieving significant space savings in a knowledge compilation perspective. More precisely, the languages FBDD and DDG of decision diagrams are extended to the languages Sym-FBDDX, Yand Sym-DDGX, Yof symmetry-driven decision diagrams, where X is a set of "symmetry-free" variables and Y is a set of "top" variables. Both the time efficiency and the space efficiency of Sym-FBDDX, Yand Sym-DDGX, Yare analyzed, in order to put those languages in the knowledge compilation map for propositional representations. It turns out that each of Sym-FBDDX, Yand Sym-DDGX, Ysatisfies CT (the model counting query). We prove that no propositional language over a set X∪ Y of variables, satisfying both CO (the consistency query) and CD (the conditioning transformation), is at least as succinct as any of Sym-FBDDX, Yand Sym-DDGX, Yunless the polynomial hierarchy collapses. The price to be paid is that only a restricted form of conditioning and a restricted form of forgetting are offered by Sym-FBDDX, Yand Sym-DDGX, Y. Nevertheless, this proves sufficient for a number of applications, including configuration and planning. We describe a compiler targeting Sym-FBDDX, Yand Sym-DDGX, Yand give some experimental results on planning domains, highlighting the practical significance of these languages.

Details

SAT Conference 2013 Conference Paper

Factoring Out Assumptions to Speed Up MUS Extraction

  • Jean-Marie Lagniez
  • Armin Biere

Abstract In earlier work on a limited form of extended resolution for CDCL based SAT solving, new literals were introduced to factor out parts of learned clauses. The main goal was to shorten clauses, reduce proof size and memory usage and thus speed up propagation and conflict analysis. Even though some reduction was achieved, the effectiveness of this technique was rather modest for generic SAT solving. In this paper we show that factoring out literals is particularly useful for incremental SAT solving, based on assumptions. This is the most common approach for incremental SAT solving and was pioneered by the authors of MINISAT. Our first contribution is to focus on factoring out only assumptions, and actually all eagerly. This enables the use of compact dedicated data structures, and naturally suggests a new form of clause minimization, our second contribution. As last main contribution, we propose to use these data structures to maintain a partial proof trace for learned clauses with assumptions, which gives us a cheap way to flush useless learned clauses. In order to evaluate the effectiveness of our techniques we implemented them within the version of MINISAT used in the publically available state-of-the-art MUS extractor MUSer. An extensive experimental evaluation shows that factoring out assumptions in combination with our novel clause minimization procedure and eager clause removal is particularly effective in reducing average clause size, improves running time and in general the state-of-the-art in MUS extraction.

Details

SAT Conference 2013 Conference Paper

Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction

  • Gilles Audemard
  • Jean-Marie Lagniez
  • Laurent Simon 0001

Abstract Beside the important progresses observed in SAT solving, a number of applications explicitly rely on incremental SAT solving only. In this paper, we focus on refining the incremental SAT Solver Glucose, from the SAT engine perspective, and address a number of unseen problems this new use of SAT solvers opened. By playing on clause database cleaning, assumptions managements and other classical parameters, we show that our approach immediately and significantly improves an intensive assumption-based incremental SAT solving task: Minimal Unsatisfiable Set. We believe this work could bring immediate benefits in a number of other applications relying on incremental SAT.

Details

IJCAI Conference 2013 Conference Paper

Just-in-Time Compilation of Knowledge Bases

  • Gilles Audemard
  • Jean-Marie Lagniez
  • Laurent Simon

Since the first principles of Knowledge Compilation (KC), most of the work has been focused in finding a good compilation target language in terms of compromises between compactness and expressiveness. The central idea remains unchanged in the last fifteen years: an off-line, very hard, stage, allows to “compile” the initial theory in order to guarantee (theoretically) an efficient on-line stage, on a set of predefined queries and operations. We propose a new “Just-in-Time” approach for KC. Here, any Knowledge Base (KB) will be immediately available for queries, and the effort spent on past queries will be partly amortized for future ones. To guarantee efficient answers, we rely on the tremendous progresses made in the practical solving of SAT and incremental SAT applicative problems. Even if each query may be theoretically hard, we show that our approach outperforms previous KC approaches on the set of classical problems used in the field, and allows to handle problems that are out of the scope of current approaches.

PDF Details DOI

IJCAI Conference 2013 Conference Paper

Knowledge Compilation for Model Counting: Affine Decision Trees

  • Frédéric Koriche
  • Jean-Marie Lagniez
  • Pierre Marquis
  • Samuel Thomas

Counting the models of a propositional formula is a key issue for a number of AI problems, but few propositional languages offer the possibility to count models efficiently. In order to fill the gap, we introduce the language EADT of (extended) affine decision trees. An extended affine decision tree simply is a tree with affine decision nodes and some specific decomposable conjunction or disjunction nodes. Unlike standard decision trees, the decision nodes of an EADT formula are not labeled by variables but by affine clauses. We study EADT, and several subsets of it along the lines of the knowledge compilation map. We also describe a CNF-to-EADT compiler and present some experimental results. Those results show that the EADT compilation-based approach is competitive with (and in some cases is able to outperform) the model counter Cachet and the d-DNNF compilationbased approach to model counting.

PDF Details DOI

IJCAI Conference 2013 Conference Paper

Preserving Partial Solutions while Relaxing Constraint Networks

  • Éric Grégoire
  • Jean-Marie Lagniez
  • Bertrand Mazure

An extension of the CSP optimization framework tailored to identify fair solutions to instances involving multiple optimization functions is studied. Two settings are considered, based on the maximization of the minimum value over all the given functions (MAX-MIN approach) and on its lexicographical refinement where, over all solutions maximizing the minimum value, those maximizing the second minimum value are preferred, and so on, until all functions are considered (LEXMAX-MIN approach). For both settings, the complexity of computing an optimal solution is analyzed and the tractability frontier is charted for acyclic instances, w. r. t. the number and the domains of the functions to be optimized. Larger islands of tractability are then identified via a novel structural approach, based on a notion of guard that is designed to deal with the interactions among constraint scopes and optimization functions.

PDF Details DOI

IJCAI Conference 2013 Conference Paper

Preserving Partial Solutions while Relaxing Constraint Networks

  • Éric Grégoire
  • Jean-Marie Lagniez
  • Bertrand Mazure

This paper is about transforming constraint networks to accommodate additional constraints in specific ways. The focus is on two intertwined issues. First, we investigate how partial solutions to an initial network can be preserved from the potential impact of additional constraints. Second, we study how more permissive constraints, which are intended to enlarge the set of solutions, can be accommodated in a constraint network. These two problems are studied in the general case and the light is shed on their relationship. A case study is then investigated where a more permissive additional constraint is taken into account through a form of network relaxation, while some previous partial solutions are preserved at the same time.

PDF Details DOI

SAT Conference 2012 Conference Paper

Revisiting Clause Exchange in Parallel SAT Solving

  • Gilles Audemard
  • Benoît Hoessen
  • Saïd Jabbour
  • Jean-Marie Lagniez
  • Cédric Piette

Abstract Managing learnt clause database is known to be a tricky task in SAT solvers. In the portfolio framework, the collaboration between threads through learnt clause exchange makes this problem even more difficult to tackle. Several techniques have been proposed in the last few years, but practical results are still in favor of very limited collaboration, or even no collaboration at all. This is mainly due to the difficulty that each thread has to manage a large amount of learnt clauses generated by the other workers. In this paper, we propose new efficient techniques for clause exchanges within a parallel SAT solver. In contrast to most of the current clause exchange methods, our approach relies on both export and import policies, and makes use of recent techniques that proves very effective in the sequential case. Extensive experimentations show the practical interest of the proposed ideas.

Details

SAT Conference 2011 Conference Paper

On Freezing and Reactivating Learnt Clauses

  • Gilles Audemard
  • Jean-Marie Lagniez
  • Bertrand Mazure
  • Lakhdar Saïs

Abstract In this paper, we propose a new dynamic management policy of the learnt clause database in modern sat solvers. It is based on a dynamic freezing and activation principle of the learnt clauses. At a given search state, using a relevant selection function, it activates the most promising learnt clauses while freezing irrelevant ones. In this way, clauses learned at previous steps can be frozen at the current step and might be activated again in future steps of the search process. Our strategy tries to exploit pieces of information gathered from the past to deduce the relevance of a given clause for the remaining search steps. This policy contrasts with all the well-known deletion strategies, where a given learned clause is definitely eliminated. Experiments on sat instances taken from the last competitions demonstrate the efficiency of our proposed technique.

Details
v2026.09.13