Publications

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), august 2017.
[BibTeX]



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, september 2016.
[BibTeX]

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, july 2016.
[BibTeX]



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, september 2014.
[pdf] [BibTeX]

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, july 2014. (Best student paper award)
[pdf] [BibTeX]

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), july 2014.
[pdf] [BibTeX]

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), june 2014.
[pdf] [BibTeX]

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, february 2014.
[pdf] [BibTeX]

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.
[pdf] [BibTeX]

Gilles Audemard, Armin Biere, Jean-Marie Lagniez, Laurent Simon, "Améliorer SAT dans le cadre incrémental". in Revue d'intelligence artificielle (RIA), vol. 28, n° 5, pp. 593-614, 2014.
[BibTeX]



2013

Gilles Audemard, Jean-Marie Lagniez, Laurent Simon, "Just-In-Time Compilation of Knowledge Bases". in 23rd International Joint Conference on Artificial Intelligence (IJCAI'13), pp. 447--453, august 2013.
[pdf] [BibTeX]

Gilles Audemard, Benoît Hoessen, Saïd Jabbour, Jean-Marie Lagniez, Cédric Piette, "PeneLoPe in SAT Competition 2013". Technical report, Helsinki, may 2013.
[pdf] [BibTeX]

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, pp. 309-317, 2013.
[pdf] [BibTeX]

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

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



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, pp. 118-126, october 2012.
[pdf] [BibTeX]

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

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, pp. 200--213, may 2012.
[pdf] [BibTeX]

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, may 2012.
[pdf] [BibTeX]

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, may 2012. (https://helda.helsinki.fi/handle/10138/34218)
[pdf] [BibTeX]



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, pp. 188-200, june 2011. (Best paper award)
[pdf] [BibTeX]



2010

Gilles Audemard, "Résolution de problèmes autour de SAT". Habilitation à Diriger des Recherches, Université d'atois, november 2010.
[pdf] [BibTeX]

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, pp. 474--488, october 2010.
[pdf] [BibTeX]

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, july 2010.
[pdf] [BibTeX]

Gilles Audemard, Jean-Marie Lagniez, Bertrand Mazure, Lakhdar Saïs, "SatHYS: Sat Hybrid Solver". Technical report, Proceedings of SAT Race 2010: Solver and Benchmarks Descriptions, Edinburgh, Scotland, UK, july 2010.
[pdf] [BibTeX]

Gilles Audemard, Jean-Marie Lagniez, Bertrand Mazure, Lakhdar Saïs, "RCL: Reduce learnt clauses". Technical report, Proceedings of SAT Race 2010: Solver and Benchmarks Descriptions, Edinburgh, Scotland, UK, july 2010.
[pdf] [BibTeX]

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, june 2010.
[pdf] [BibTeX]

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, january 2010.
[pdf] [BibTeX]



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, november 2009.
[pdf] [BibTeX]

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), september 2009. (dans le cadre de CP'09)
[pdf] [BibTeX]

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, july 2009.
[pdf] [BibTeX]

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, june 2009.
[pdf] [BibTeX]

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, june 2009.
[pdf] [BibTeX]



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, pp. 630--634, september 2008.
[pdf] [BibTeX]

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, june 2008.
[pdf] [BibTeX]

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, pp. 21--27, may 2008.
[BibTeX]

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

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.
[pdf] [BibTeX]



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), september 2007.
[BibTeX]

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), july 2007.
[pdf] [BibTeX]

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, may 2007.
[pdf] [BibTeX]

Gilles Audemard, Laurent Simon, "GUNSAT : a greedy local search algorithm for unsatisfiability". in International Joint Conference on Artificial Intelligence (IJCAI'07), pp. 2256--2261, january 2007.
[pdf] [BibTeX]

Gilles Audemard, Saïd Jabbour, Lakhdar Saïs, " Symmetry Breaking in Quantified Boolean Formulae". in International Joint Conference on Artificial Intelligence (IJCAI'07), pp. 2262--2267, january 2007.
[pdf] [BibTeX]



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, december 2006.
[pdf] [BibTeX]

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, june 2006.
[pdf] [BibTeX]



2005

Gilles Audemard, Lakhdar Saïs, "Une approche symbolique pour les formules booléennes quantifiées". in 1ères Journées Francophones de Programmation par Contraintes (JFPC'05), pp. 59-68, june 2005.
[pdf] [BibTeX]

Gilles Audemard, Marco Bozzano, Alessandro Cimatti, Roberto Sebastiani, "Verifying Industrial Hybrid Systems with MathSAT". in Electronic Notes in Theoretical Computer Science , vol. 119, n° 2, pp. 17--32, march 2005.
[pdf] [BibTeX]

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

Gilles Audemard, Lakhdar Saïs, " Une approche Symbolique pour les Formules Booléennes Quantifiées". in Colloque sur l'Optimisation et les Systèmes d'Information (COSI'05), pp. 285-296, 2005.
[BibTeX]



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, september 2004.
[pdf] [BibTeX]

Gilles Audemard, Bertrand Mazure, Lakhdar Saïs, " Dealing with Symmetries in Quantified Boolean Formulas". in Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT'04), pp. 257-262, 2004.
[pdf] [BibTeX]

Gilles Audemard, Bertrand Mazure, Lakhdar Saïs, " Symétries et Formules Booléennes Quantifiées". in 10èmes Journées Nationales sur la résolution pratique des Problèmes NP-Complets (JNPC'04), pp. 43 - 53, 2004.
[pdf] [BibTeX]



2003

Gilles Audemard, Daniel Le berre, Olivier Roussel, "OpenSAT: une plateforme SAT Open Source". in 9èmes Journées Nationales sur la résolution pratique des problèmes NP-complets (JNPC'03), june 2003.
[pdf] [BibTeX]

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 (SAT'03), may 2003. (poster)
[pdf] [BibTeX]

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.
[BibTeX]



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, november 2002.
[pdf] [BibTeX]

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, july 2002.
[pdf] [BibTeX]

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, july 2002.
[pdf] [BibTeX]

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

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 , july 2002.
[BibTeX]



2001

Gilles Audemard, Belaid Benhamou, "Symmetry in finite model of first order logic". in Workshop on Symmetry and Constraint Satisfaction Problems - Affiliated to CP (SymCon), pp. 01-08, december 2001.
[pdf] [BibTeX]

Gilles Audemard, " Résolution du problème SAT et génération de modèles finis en logique du premier ordre". PhD Thesis, Provence, october 2001.
[BibTeX]

Gilles Audemard, Laurent Henocque, " The eXtended Least Number Heuristic". in International Joint Conference on Automated Reasoning (IJCAR'01), Springer, pp. 427-442, june 2001.
[pdf] [BibTeX]

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, april 2001.
[pdf] [BibTeX]



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, july 2000.
[pdf] [BibTeX]

Gilles Audemard, Belaid Benhamou, Laurent Henocque, " Two techniques to improve Finite Model Search.". in 17th Conference on Automated Deduction (CADE'17), LNCS 2083, Springer Verlag, pp. 302-308, june 2000.
[pdf] [BibTeX]

Gilles Audemard, Laurent Henocque, " Sur la génération des groupes finis non isomorphes". in 6èmes Journées Nationales sur la Résolution Pratique des Problèmes NP-complets (JNPC'00), pp. 57-66, june 2000.
[pdf] [BibTeX]



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, june 1999.
[pdf] [BibTeX]