Publications

Article(s) de revue(s) internationale(s)

2014 Gilles Audemard, Armin Biere, Jean-Marie Lagniez, Laurent Simon, Améliorer SAT dans le cadre incrémental in Revue d’Intelligence Artificielle,vol. 28, n° 5, pp. 593-614, 2014.

2008 Gilles Audemard, Saïd Jabbour, Lakhdar Saïs, SAT Graph-Based Representation: A New Perspective in Journal of Algorithms,vol. 63, pp. 17–33, 2008. [Download]

2006 Gilles Audemard, Belaid Benhamou, Laurent Henocque, Predicting and Detecting Symmetries in FOL Finite Model Search in Journal of Automated Reasoning,vol. 36, n° 3, pp. 177–212, decembre 2006. [Download]

2005 Gilles Audemard, Marco Bozzano, Alessandro Cimatti, Roberto Sebastiani, Verifying Industrial Hybrid Systems with MathSAT in Second International Workshop on Bounded Model Checking,vol. 119, n° 2, pp. 17–32, mars 2005. [Download]

Article(s) de conférence(s) internationale(s)

2017 Gilles Audemard, Jean-Marie Lagniez, Nicolas Szczepanski, Sébastien Tabary, A Distributed Version of Syrup in 20th International Conference on Theory and Applications of Satisfiability Testing (SAT’17),août 2017.

2016 Gilles Audemard, Laurent Simon, Extreme Cases in SAT Problems in Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference (SAT’16),Lecture Notes in Computer Science (LNCS) Volume 9710, Springer, pp. 87-103, juillet 2016.

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

2014 Gilles Audemard, Laurent Simon, Lazy Clause Exchange Policy for parallel SAT solvers in 17th International Conference on Theory and Applications of Satisfiability Testing (SAT’14),pp. 197-205, 2014.

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

2014 Zack Newsham, Vijay Ganesh, Sebastian Fischmeister, Gilles Audemard, Laurent Simon, Impact of Community Structure on SAT Solver Performance in 17th International Conference on Theory and Applications of Satisfiability Testing (SAT’14),pp. 252-268, juillet 2014. (Best student paper award)

2014 Gilles Audemard, Benoît Hoessen, Saïd Jabbour, Cédric Piette, An Effective Distributed D&C Approach for the Satis?ability Problem in 22nd International Conference on Parallel, Distributed and Network-Based Computing (PDP’14),pp. 183-187, février 2014.

2014 Gilles Audemard, Christophe Lecoutre, Mouny Samy-Modeliar, Gilles Goncalves, Daniel Porumbel, Scoring-based Neighborhood Dominance for the Subgraph isomorphism Problem in 20th International Conference on Principles and Practice of Constraint Programming (CP’14),Lecture Notes in Computer Science (LNCS), Volume 8656, Springer, pp. 125–141, septembre 2014. [Download]

2013 Gilles Audemard, Jean-Marie Lagniez, Laurent Simon, Just-In-Time Compilation of Knowledge Bases in 23th International Joint Conference on Artificial Intelligence (IJCAI’13),pp. 447–453, août 2013. [Download]

2013 Gilles Audemard, Jean-Marie Lagniez, Laurent Simon, Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction in 16th International Conference on Theory and Applications of Satisfiability Testing (SAT’13),Springer, Lecture Notes in Computer Science, vol. 7962, pp. 309-317, 2013.

2012 Gilles Audemard, Laurent Simon, GLUCOSE 2.1: Aggressive, but Reactive, Clause Database Management, Dynamic Restarts (System Description) in Pragmatics of SAT 2012 (POS’12),juin 2012. (dans le cadre de SAT’2012)

2012 Gilles Audemard, Benoît Hoessen, Saïd Jabbour, Jean-Marie Lagniez, Cédric Piette, PeneLoPe, a Parallel Clause-Freezer Solver in Proceedings of SAT Challenge 2012: Solver and Benchmarks Descriptions,pp. 43–44, mai 2012. (https://helda.helsinki.fi/handle/10138/34218)

2012 Gilles Audemard, Benoît Hoessen, Saïd Jabbour, Jean-Marie Lagniez, Cédric Piette, Revisiting Clause Exchange in Parallel SAT Solving in 15th International Conference on Theory and Applications of Satisfiability Testing (SAT’12),Springer, Lecture Notes in Computer Science(LNCS), vol. 7962, pp. 200–213, mai 2012.

2012 Gilles Audemard, Laurent Simon, Refining Restarts Strategies For SAT and UNSAT in 18th International Conference on Principles and Practice of Constraint Programming (CP’12),Springer, Lecture Notes in Computer Science (LNCS), vol. 7514, pp. 118-126, octobre 2012.

2011 Gilles Audemard, Jean-Marie Lagniez, Bertrand Mazure, Lakhdar Saïs, On freezeing and reactivating learnt clauses in 14th International Conference on Theory and Applications of Satisfiability Testing (SAT’11),Springer, Lecture Notes in Computer Science (LNCS), vol. 6695, pp. 188-200, juin 2011. (Best paper award)

2010 Gilles Audemard, George Katsirelos, Laurent Simon, A Restriction of Extended Resolution for Clause Learning SAT Solvers in 24th Conference on Artificial Intelligence (AAAI’10),pp. 10–15, juillet 2010. [Download]

2010 Gilles Audemard, Jean-Marie Lagniez, Bertrand Mazure, Lakhdar Saïs, Boosting local search thanks to CDCL in 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR’10),Springer, Lecture Notes in Computer Science (LNCS), vol. 6397, pp. 474–488, octobre 2010.

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

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

2009 Gilles Audemard, Laurent Simon, Predicting Learnt Clauses Quality in Modern SAT Solver in 21st International Joint Conference on Artificial Intelligence (IJCAI’09),pp. 399-404, juillet 2009. [Download]

2008 Gilles Audemard, Laurent Simon, Experimenting a Conflict-Driven Clause Learning Algorithm in 14th International Conference on Principles and Practice of Constraint Programming (CP’08),Springer, Lecture Notes in Computer Science (LNCS), vol. 5202, pp. 630–634, septembre 2008.

2008 Gilles Audemard, Lucas Bordeaux, Youssef Hamadi, Saïd Jabbour, Lakhdar Saïs, A generalized Framework For Conflict Analysis in 11th International Conference on Theory and Applications of Satisfiability Testing (SAT’08),Springer, Lecture Notes in Computer Science (LNCS), vol. 4996, pp. 21–27, mai 2008.

2007 Gilles Audemard, Saïd Jabbour, Lakhdar Saïs, Using SAT-Graph representation to derive hard instances in 14th RCRA workshop Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion (RCRA’07),juillet 2007.

2007 Gilles Audemard, Laurent Simon, GUNSAT : a greedy local search algorithm for unsatisfiability in International Joint Conference on Artificial Intelligence (IJCAI’2007),pp. 2256–2261, janvier 2007. [Download]

2007 Gilles Audemard, Saïd Jabbour, Lakhdar Saïs, Symmetry Breaking in Quantified Boolean Formulae in International Joint Conference on Artificial Intelligence (IJCAI’2007),pp. 2262–2267, janvier 2007. [Download]

2007 Gilles Audemard, Saïd Jabbour, Lakhdar Saïs, Efficient Symmetry breaking Predicates for quantified boolean formulae in Workshop on Symmetry and Constraint Satisfaction Problems - Affiliated to CP (SymCon),septembre 2007.

2007 Gilles Audemard, Lakhdar Saïs, Circuit Based Encoding of CNF Formula in Tenth International Conference on Theory and Applications of Satisfiability Testing (SAT’07),LNCS 4501, Springer Verlag, pp. 16–21, mai 2007.

2005 Gilles Audemard, Lakhdar Saïs, A Symbolic Search Based Approach for Quantified Boolean Formulas in Proceedings of the 8th International Conference on Theory and Applications of Satisfiability Testing (SAT’05), LNCS 3569, Springer Verlag, pp. 16-30, 2005.

2005 Gilles Audemard, Lakhdar Saïs, Une approche Symbolique pour les Formules Booléennes Quantifiées in Actes du Colloque sur l?Optimisation et les Systèmes d?Informations (COSI’05),pp. 285-296, 2005.

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

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

2003 Gilles Audemard, Marco Bozzano, Alessandro Cimatti, Roberto Sebastiani, Verifying Industrial Hybrid Systems with MathSAT in Proceedings of the first workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR),pp. 62-75, 2003.

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

2002 Gilles Audemard, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani, Bounded Model Checking for Timed Systems in 22nd International Conference on Formal Techniques for Networked and Distributed Systems (FORTE’02),LNCS 2529 Springer Verlag, pp. 243-259, novembre 2002.

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

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

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

2002 Gilles Audemard, Belaid Benhamou, Reasoning by symmetry and function ordering in Finite model generation in 18th Conference on Automated Deduction (CADE’18),LNCS 2392 Springer Verlag, pp. 226-240, juillet 2002.

2001 Gilles Audemard, Laurent Henocque, The eXtended Least Number Heuristic in International Joint Conference on Automated Reasoning (IJCAR’01),Springer, LNAI 2083, pp. 427-442, juin 2001.

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

2000 Gilles Audemard, Belaid Benhamou, Laurent Henocque, Two techniques to improve Finite Model Search. in Proceedings of the 17th International Conference on Automated Deduction (CADE 17),LNCS 2083, Springer Verlag, LNCS 1831, pp. 302-308, juin 2000.

2000 Gilles Audemard, Belaid Benhamou, Pierre Siegel, AVAL: an Enumerative Method for SAT in International Conference on Computational Logic (CL’00),LNCS 1861, Springer Verlag, pp. 373-383, juillet 2000.

Article(s) de conférence(s) nationale(s)

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

2013 Gilles Audemard, Jean-Marie Lagniez, Laurent Simon, Du glucose en goutte à goutte pour les coeurs insatisfiables in 9ièmes Journées Francophones de Programmation par Contraintes (JFPC’13),pp. 59-66, 2013. [Download]

2013 Gilles Audemard, Benoît Hoessen, Saïd Jabbour, Cédric Piette, Un nouveau cadre diviser pour régner pour SAT distribué in 9ièmes Journées Francophones de Programmation par Contraintes (JFPC’13),pp. 51-58, 2013. [Download]

2012 Gilles Audemard, Benoît Hoessen, Saïd Jabbour, Jean-Marie Lagniez, Cédric Piette, Résolution parallèle de SAT : mieux collaborer pour aller plus loin in 8ièmes Journées Francophones de Programmation par Contraintes (JFPC’12),pp. 35–44, mai 2012.

2010 Gilles Audemard, Jean-Marie Lagniez, Bertrand Mazure, Approche hybride pour SAT in 17ième Congrès Francophone sur la Reconnaissance des Formes et Intelligence Artificielle (RFIA’10),pp. 279–286, janvier 2010. [Download]

2010 Gilles Audemard, George Katsirelos, Laurent Simon, Une restriction de la résolution étendue pour les démonstrateurs SAT modernes in 6ièmes Journées Francophones de Programmation par Contraintes (JFPC’10),pp. 43–50, juin 2010. [Download]

2009 Gilles Audemard, Jean-Marie Lagniez, Bertrand Mazure, Lakhdar Saïs, Analyse de conflits dans le cadre de la recherche locale in 5ièmes Journées Francophones de la Programmation par Contraintes (JFPC’09),pp. 215-224, juin 2009. [Download]

2009 Gilles Audemard, Mouny Samy-Modeliar, Laurent Simon, Pourquoi les solveurs SAT modernes se piquent-ils contre des cactus ? in 5ièmes Journées Francophones de la Programmation par Contraintes (JFPC’09),pp. 245-253, juin 2009. [Download]

2008 Gilles Audemard, Lucas Bordeaux, Youssef Hamadi, Saïd Jabbour, Lakhdar Saïs, Un cadre général pour l’analyse des conflits in 4ièmes Journées Francophones de Programmation par Contraintes (JFPC’08),pp. 267–276, juin 2008. [Download]

2006 Gilles Audemard, Saïd Jabbour, Lakhdar Saïs, Exploitation des symétries dans les formules booléennes quantifiées in 2ndes Journées Francophones de Programmation par Contraintes (JFPC’06),pp. 257–266, juin 2006.

2005 Gilles Audemard, Lakhdar Saïs, Une approche symbolique pour les formules booléennes quantifiées in Premières Journées Francophones de la Programmation par Contraintes (JFPC’05),pp. 59-68, juin 2005.

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

2003 Gilles Audemard, Daniel Le Berre, Olivier Roussel, OpenSAT: une plateforme SAT Open Source in JNPC’03,juin 2003. [Download]

2001 Gilles Audemard, Belaid Benhamou, Etude des symétries dans les modèles finis in 11èmes Journées Francophones de Programmation en Logique et programmation par Containtes (JFPLC’01),Hermes Science, pp. 109-122, avril 2001.

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

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

Chapitre(s) d'ouvrage(s)

2008 Gilles Audemard, Belaid Benhamou, Symétries in Problème SAT : progrès et défis,chapitre 6, Lakhdar Saïs (Eds.), Hermes, 2008.

Thèse(s) de doctorat

2001 Gilles Audemard, Résolution du problème SAT et génération de modèles finis en logique du premier ordre Provence, octobre 2001.

Habilitation(s) à Diriger des Recherches

2010 Gilles Audemard, Résolution de problèmes autour de SAT Université d’atois, novembre 2010.

Rapport(s) technique(s)

2013 Gilles Audemard, Benoît Hoessen, Saïd Jabbour, Jean-Marie Lagniez, Cédric Piette, PeneLoPe in SAT Competition 2013 Helsinki, mai 2013. [Download]

2010 Gilles Audemard, Jean-Marie Lagniez, Bertrand Mazure, Lakhdar Saïs, SatHYS: Sat Hybrid Solver Proceedings of SAT Race 2010: Solver and Benchmarks Descriptions, Edinburgh, Scotland, UK, juillet 2010.

2010 Gilles Audemard, Jean-Marie Lagniez, Bertrand Mazure, Lakhdar Saïs, RCL: Reduce learnt clauses Proceedings of SAT Race 2010: Solver and Benchmarks Descriptions, Edinburgh, Scotland, UK, juillet 2010.