Publications

2023

Gilles Audemard, Jean-Marie Lagniez, Pierre Marquis, Nicolas Szczepanski. On Contrastive Explanations for Tree-Based Classifiers. The 26th European Conference on Artificial Intelligence (ECAI'23), Sep 2023, Cracovie, Poland.

Gilles Audemard, Jean-Marie Lagniez, Pierre Marquis, Nicolas Szczepanski. Deriving Explanations for Decision Trees: The Impact of Domain Theories, 2023. ⟨hal-04176274⟩.

Gilles Audemard, Jean-Marie Lagniez, Pierre Marquis, Nicolas Szczepanski. Computing Abductive Explanations for Boosted Trees. 26th International Conference on Artificial Intelligence and Statistics (AISTATS 2023), pages 4699-4711, 2023.

Gilles Audemard, Steve Bellart, Louenas Bounia, Jean-Marie Lagniez, Pierre Marquis, Nicolas Szczepanski. PyXAI : calculer en Python des explications pour des modèles d'apprentissage supervisé. Extraction et Gestion des Connaissances, EGC, pages 581-588, 2023.

Gilles Audemard, Steve Bellart, Louenas Bounia, Frederic Koriche, Jean-Marie Lagniez, Pierre Marquis. Sur les explications abductives préférées pour les arbres de décision et les forêts aléatoires. Extraction et Gestion des Connaissances, EGC, pages 507-514, 2023.

Gilles Audemard, Christophe Lecoutre, Charles Prud'Homme. Guiding Backtrack Search by Tracking Variables During Constraint Propagation. International Conference on Principles and Practice of Constraint Programming, pages 1-9, 2023.


2022

Gilles Audemard, Christophe Lecoutre, Emmanuel Lonca. Proceedings of the 2022 XCSP3 Competition, Arxiv, 2022. .

Gilles Audemard, Jean-Marie Lagniez, Marie Miceli. A New Exact Solver for (Weighted) Max#SAT. International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 1-20, 2022.

Gilles Audemard, Steve Bellart, Louenas Bounia, Frederic Koriche, Jean-Marie Lagniez, Pierre Marquis. On Preferred Abductive Explanations for Decision Trees and Random Forests. Thirty-First International Joint Conference on Artificial Intelligence (IJCAI), pages 643-650, 2022.

Gilles Audemard, Steve Bellart, Louenas Bounia, Frédéric Koriche, Jean-Marie Lagniez, Pierre Marquis. Trading Complexity for Sparsity in Random Forest Explanations. AAAI Conference on Artificial Intelligence, pages 5461-5469, 2022.

Gilles Audemard, Jean-Marie Lagniez, Marie Miceli, Olivier Roussel. Identifying Soft Cores in Propositional Formulae. 14th International Conference on Agents and Artificial Intelligence, ICAART, pages 486-495, 2022.

Gilles Audemard, Steve Bellart, Louenas Bounia, Frédéric Koriche, Jean-Marie Lagniez et Pierre Marquis. Sur le pouvoir explicatif des arbres de décision. Extraction et Gestion des Connaissances, EGC, pages 147-158, 2022.

Gilles Audemard, Steve Bellart, Louenas Bounia, Frédéric Koriche, Jean-Marie Lagniez, pierre Marquis. Les raisons majoritaires : des explications abductives pour les forêts aléatoires. 22ème Conférence francophone sur l'Extraction et Gestion des Connaissances, EGC, pages 123-134, 2022.

Gilles Audemard, Steve Bellart, Louenas Bounia, Frédéric Koriche, Jean-Marie Lagniez, Pierre Marquis. On the Explanatory Power of Boolean Decision Trees. Data and Knowledge Engineering, 2022.


2021

Frederic Boussemart, Christophe Lecoutre, Gilles Audemard, Cédric Piette. XCSP3: An Integrated Format for Benchmarking Combinatorial Constrained Problems. [Technical Report] ArXiv.

Gilles Audemard, Steve Bellart, Louenas Bounia, Frédéric Koriche, Jean-Marie Lagniez, Pierre Marquis. On the Computational Intelligibility of Boolean Classifiers. 18th International Conference on Principles of Knowledge Representation and Reasoning (KR), pages 74-86, 2021.

Nicolas Szczepanski, Gilles Audemard, Laetitia Jourdan, Christophe Lecoutre, Lucien Mousin, Nadarajen Veerapen. A hybrid CP/MOLS approach for multi-objective imbalanced classification. GECCO '21: Genetic and Evolutionary Computation Conference, pages 723-731, 2021.

Frédéric Boussemart, Christophe Lecoutre, Gilles Audemard, Cédric Piette. XCSP3-core: A Format for Representing Constraint Satisfaction/Optimization Problems. [Technical Report] ArXiv.


2020

Gilles Audemard, Loïc Paulevé, Laurent Simon. SAT Heritage: a community-driven effort for archiving, building and running more than thousand SAT solvers. SAT, The 23rd International Conference on Theory and Applications of Satisfiability Testing, pages 107-113, 2020.

Gilles Audemard, Christophe Lecoutre, Mehdi Maamar. Segmented Tables: an Efficient Modeling Tool for Constraint Reasoning. 24th European Conference on Artificial Intelligence (ECAI'20), pages 315-322, 2020.

Gilles Audemard, Frédéric Boussemart, Christophe Lecoutre, Cédric Piette, Olivier Roussel. XCSP3 and its ecosystem. Constraints Journal (Constraints), pages 47-69, 2020.

Gilles Audemard, Frédéric Koriche, Pierre Marquis. On Tractable XAI Queries based on Compiled Representations. 17th International Conference on Principles of Knowledge Representation and Reasoning (KR), pages 838-849, 2020.


2019

Gilles Audemard, Gael Glorian, Jean-Marie Lagniez, Valentin Montmirail, Nicolas Szczepanski. pFactory: A generic library for designing parallel solvers. International Conference on Applied Computing (AC), 2019.


2018

Gilles Audemard, Laurent Simon. On the Glucose SAT solver. International Journal on Artificial Intelligence Tools (IJAIT), 27 (1), pages 1-25, 2018.


2017

Gilles Audemard, Jean-Marie Lagniez, Nicolas Szczepanski, Sébastien Tabary. A Distributed Version of Syrup. 20th International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 215-232, 2017.


2016

Gilles Audemard, Jean-Marie Lagniez, Nicolas Szczepanski, Sébastien Tabary. An Adaptive SAT Solver. 22nd International Conference on Principles and Practice of Constraint Programming (CP'16), pages 30-48, 2016.

Gilles Audemard, Laurent Simon. Extreme Cases in SAT Problems. 19th International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 87-103, 2016.


2014

Gilles Audemard, Laurent Simon. Lazy clause exchange policy for parallel SAT solvers. 17th International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 197-205, 2014.

Zack Newsham, Gilles Audemard, Vijay Ganesh, Sebastian Fischmeister, Laurent Simon. Impact of Community Structure on SAT Solver Performance. 17th International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 252-268, 2014.

Gilles Audemard, Christophe Lecoutre, Mouny Samy-Modeliar, Gilles Goncalves, Daniel Porumbel. Dominance au voisinage pour le probleme d'isomorphisme de sous-graphe. 8èmes Journées Nationales de l'Intelligence Artificielle Fondamentale (IAF'14), 2014, Angers, France.

Gilles Audemard, Armin Biere, Jean-Marie Lagniez, Laurent Simon. Améliorer SAT dans le cadre incrémental. Revue d'intelligence artificielle (RIA), 28 (5), pages 593-614, 2014.

Gilles Audemard, Benoît Hoessen, Saïd Jabbour, Cédric Piette. An Effective Distributed D&C Approach for the Satisfiability Problem. 22nd International Conference on Parallel, Distributed and Network-Based Computing (PDP), pages 183-187, 2014.

Gilles Audemard, Benoît Hoessen, Saïd Jabbour, Cédric Piette. Dolius: A Distributed Parallel SAT Solving Framework. Pragmatics of SAT 2014 (POS), 2014.


2013

Gilles Audemard, Jean-Marie Lagniez, Laurent Simon. Du Glucose en goutte à goutte pour les coeurs inconsistants. Journées Francophones de Programmation par Contraintes, 2013.

Gilles Audemard, Jean-Marie Lagniez, Laurent Simon. Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction. International Conference on Theory and Applications of Satisfiability Testing, pages 309-317, 2013.

Gilles Audemard, Benoît Hoessen, Said Jabbour, Cédric Piette. Un nouveau cadre diviser pour régner pour SAT distribué. 9ièmes Journées Francophones de Programmation par Contraintes (JFPC), 2013.

Gilles Audemard, Jean-Marie Lagniez, Laurent Simon. Just-In-Time Compilation of Knowledge Bases. 23th International Joint Conference on Artificial Intelligence (IJCAI), pages 447-453, 2013.


2012

Gilles Audemard, Laurent Simon. Refining restarts strategies for SAT and UNSAT formulae. 18th International Conference on Principles and Practice of Constraint Programming, pages 118-126, 2012.

Gilles Audemard, Laurent Simon. Glucose 2. 1: Aggressive - but Reactive - Clause Database Management, Dynamic Restarts.

Gilles Audemard, Laurent Simon. GLUCOSE 2. 1: Aggressive, but Reactive, Clause Database Management, Dynamic Restarts (System Description).

Gilles Audemard, Benoît Hoessen, Said Jabbour, Jean-Marie Lagniez, Cédric Piette. Résolution parallèle de SAT : mieux collaborer pour aller plus loin. 8ièmes Journées Francophones de Programmation par Contraintes (JFPC), 2012.

Gilles Audemard, Benoît Hoessen, Said Jabbour, Jean-Marie Lagniez, Cédric Piette. Revisiting Clause Exchange in Parallel SAT Solving. 15th International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 200-213, 2012.

Gilles Audemard, Benoît Hoessen, Said Jabbour, Jean-Marie Lagniez, Cédric Piette. Résolution parallèle de SAT: mieux collaborer pour aller plus loin. (JFPC), 2012.

Gilles Audemard, Benoît Hoessen, Said Jabbour, Jean-Marie Lagniez, Cédric Piette. PeneLoPe, a Parallel Clause-Freezer Solver. SAT Challenge: Solver and Benchmarks Descriptions, 2012.


2011

Gilles Audemard, Jean-Marie Lagniez, Bertrand Mazure, Lakhdar Saïs. On freezeing and reactivating learnt clauses. 14th International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 188-200, 2011.


2010

Laurent Simon, Gilles Audemard, George Katsirelos. Une restriction de la résolution étendue pour les démonstrateurs SAT modernes. (JFPC), 2010.

Gilles Audemard, Jean-Marie Lagniez, Bertrand Mazure. Approche hybride pour SAT. 17ième Congrès Francophone sur la Reconnaissance des Formes et Intelligence Artificielle (RFIA), pages 279-286, 2010.

Gilles Audemard, Jean-Marie Lagniez, Bertrand Mazure, Lakhdar Saïs. Boosting local search thanks to {CDCL}. 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), pages 474-488, 2010.

Gilles Audemard, George Katsirelos, Laurent Simon. A Restriction of Extended Resolution for Clause Learning SAT Solvers. 24th Conference on Artificial Intelligence (AAAI), pages 10-15, 2010.


2009

Laurent Simon, Gilles Audemard. Predicting Learnt Clauses Quality in Modern SAT Solver. Twenty-first International Joint Conference on Artificial Intelligence (IJCAI), pages 399-404, 2009.

Gilles Audemard, Jean-Marie Lagniez, Bertrand Mazure, Lakhdar Saïs. Integrating Conflict Driven Clause Learning to Local Search. 6th International Workshop on Local Search Techniques in Constraint Satisfaction (LSCS), 2009.

Gilles Audemard, Jean-Marie Lagniez, Bertrand Mazure, Lakhdar Saïs. Learning in local search. 21st International Conference on Tools with Artificial Intelligence (ICTAI), pages 417-424, 2009.

Gilles Audemard, Jean-Marie Lagniez, Bertrand Mazure, Lakhdar Saïs. Analyse de conflits dans le cadre de la recherche locale. Cinquièmes Journées Francophones de Programmation par Contraintes (JFPC), 2009.

Gilles Audemard, Mouny Samy Modeliar, Laurent Simon. Pourquoi les solveurs SAT modernes se piquent-ils contre des cactus ?. Cinquièmes Journées Francophones de Programmation par Contraintes (JFPC), 2009.


2008

Gilles Audemard, Said Jabbour, Lakhdar Saïs. SAT Graph-Based Representation: A New Perspective. Journal of Algorithms in Cognition, Informatics and Logic, (63) pages 17--33, 2008.

Gilles Audemard, Laurent Simon. Experimenting a Conflict-Driven Clause Learning Algorithm. 14th International Conference on Principles and Practice of Constraint Programming (CP), pages 630-634, 2008.

Gilles Audemard, Belaïd Benhamou. Symétries. Lakhdar Saïs, Problème SAT : progrès et défis, Hermès, pages 169-190, 2008.

Gilles Audemard, Lucas Bordeaux, Youssef Hamadi, Said Jabbour, Lakhdar Saïs. A generalized Framework For Conflict Analysis. Eleventh International Conference on Theory and Applications of Satisfiability Testing(SAT), pages 21-27, 2008.

Gilles Audemard, Lucas Bordeaux, Youssef Hamadi, Said Jabbour, Lakhdar Saïs. Un cadre général pour l'analyse des conflits. 4ièmes Journées Francophones de Programmation par Contraintes (JFPC), 2008.


2007

Gilles Audemard, Said Jabbour, Lahkdar Sais. Efficient Symmetry Breaking Predicates for Quantified Boolean Formulae. Workshop on Symmetry and Constraint Satisfaction Problems - Affiliated to CP(SymCon), pages 14-21, 2007.

Gilles Audemard, Said Jabbour, Lahkdar Sais. Using SAT-Graph representation to derive hard instances. 14th RCRA workshop Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion (RCRA), 2007.

Gilles Audemard, Said Jabbour, Lahkdar Sais. Symmetry Breaking in Quantified Boolean Formulae. International Joint Conference on Artificial Intelligence (IJCAI), pages 2262--2267, 2007.

Gilles Audemard, Lahkdar Sais. Circuit Based Encoding of CNF Formula. Tenth International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 16--21, 2007.

Gilles Audemard, L. Simon. GUNSAT: a greedy local search algorithm for unsatisfiability.


2006

Gilles Audemard, Belaïd Benhamou, Laurent Henocque. Predicting and Detecting Symmetries in FOL Finite Model Search. Journal of Automated Reasoning, 2006, 36 (3), pages 177-212.

Gilles Audemard, Said Jabbour, Lakhdar Saïs. Exploitation des symétries dans les formules booléennes quantifiées. Deuxièmes Journées Francophones de Programmation par Contraintes (JFPC), 2006.


2005

Gilles Audemard, Marco Bozzano, Alessendro Cimatti, Roberto Sebastiani. Verifying Industrial Hybrid Systems with MathSAT. Electronic Notes in Theoretical Computer Science, 119 (2), pages 17-32, 2005.

Gilles Audemard, Lahkdar Sais. A Symbolic Search Based Approach for Quantified Boolean Formulas. International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 16-30, 2005.

Gilles Audemard, Lakhdar Saïs. Une approche symbolique pour les formules booléennes quantifiées. Premières Journées Francophones de Programmation par Contraintes (JFPC), 2005.


2004

Gilles Audemard, Lakhdar Saïs. SAT Based BDD Solver for Quantified Boolean Formulas. 16th IEEE International Conference on Tools with Artificial Intelligence (ICTAI), pages 82-89, 2004.

Gilles Audemard, Bertrand Mazure, Lakhdar Saïs. Dealing with Symmetries in Quantified Boolean Formulas. Proceedings of the Seventh International Conference on Theory and Applications of Satisfiability Testing, (SAT), pages 257-262, 2004.

Gilles Audemard, Belaïd Benhamou, Laurent Henocque. Predecting and detecting symmetry in Finite Model Search. [Rapport de recherche] LSIS.

Gilles Audemard, Bertrand Mazure, Lakhdar Saïs. Symétries et Formules Booléennes Quantifiées. Journées Nationales de la Résolution Pratique des Problèmes NP-Complets (JNPC), 2004.


2003

Gilles Audemard, Daniel Le Berre, Olivier Roussel. OpenSAT: une plateforme SAT Open Source. JNPC, 2003.

Gilles Audemard, Daniel Le Berre, Olivier Roussel, Ines Lynce, Joao Marques-Silva. OpenSAT: an open source SAT software project. Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT), 2003.


2002

Gilles Audemard, Belaid Benhamou. Reasoning by symmetry and function ordering in Finite model generation. 18th Conference on Automated Deduction (CADE), pages 226-240, 2002.

Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani. Bounded model checking for timed systems. Second Workshop on Real-Time Tools-Affiliated with CAV, 2002.

Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani. Integrating boolean and mathematical solving : fondations, basic algorithms and requirements. Proceedings on the 10th Symposium on the Integration of symbolic Computation and Mechanized Reasoning (CALCULEMUS) pages 231-245, 2002.

Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani. A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions. 18th Conference on Automated Deduction (CADE), pages 195-210, 2002.

Gilles Audemard, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani. Bounded Model Checking for Timed Systems. 22nd International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), pages 243-259, 2002.


2001

Gilles Audemard, Belaid Benhamou. Etude des symétries dans les modèles finis. 11èmes Journées Francophones de Programmation en Logique et programmation par Containtes (JFPLC), 2001.

Gilles Audemard, Belaid Benhamou. Symmetry in finite model of first order logic. Proceedings of Symmetry in Constraint (SymCon'01) - CP Workshop, pages 01-08, 2001.

Gilles Audemard, Laurent Henocque. The eXtended Least Number Heuristic. International Joint Conference on Automated Reasoning (IJCAR), pages427-442, 2001.


2000

Gilles Audemard, Belaid Benhamou, Pierre Siegel. AVAL: an Enumerative Method for SAT. International Conference on Computational Logic (CL), pages 373-383, 2000.

Gilles Audemard, Belaid Benhamou, Laurent Henocque. Two techniques to improve Finite Model Search. Proceedings of the 17th International Conference on Automated Deduction (CADE), pages 302-308, 2000.

Gilles Audemard, Laurent Henocque. Sur la génération des groupes finis non isomorphes. Actes des sixièmes Journées Nationales des problèmes NP complets (JNPC), 2000.


1999

Gilles Audemard, Belaid Benhamou, Pierre Siegel. La méthode d'avalanche AVAL : une méthode énumérative pour SAT. 5èmes Journées Nationales sur la Résolution Pratique des Problèmes NP-Complets (JNPC), 1999.