contact

INRIA-Microsoft Research Joint Centre

28 rue Jean Rostand,

91893 Orsay Cedex, France

Phone : (+33) 1 69 35 69 91

Fax : (+33) 1 69 35 69 69

Email:said[dots]jabbour[at]inria[dots]fr

---

Research area

• Resolution of NP-Hard problems
• Propositional logic : models and algorithms
• Propositional Satisfiability (SAT)
• Parallel SAT
• Quantified Boolean Formulas (QBF)

---

Awards

Sat-Race 2010

• [ Youssef Hamadi , S. Jabbour and L. Sais] ManySAT 1.5, silver medal, SAT Race 2010 (Parallel solvers category)
• [ Youssef Hamadi , S. Jabbour and L. Sais] ManySAT 1.1, bronze medal, SAT Race 2010 (Parallel solvers category)

SAT competition 2009

• [ Youssef Hamadi , S. Jabbour and L. Sais] ManySAT, First rank (Jury special price), International SAT 2009 competition (Parallel Track) in Application category, June 30 - July 3, 2009, Swansea, Wales, United Kingdom
• [ Youssef Hamadi , S. Jabbour and L. Sais]. LySAT , Two bronze medal, International SAT 2009 competition (Sequential Track) in Application category (SAT-UNSAT and UNSAT), June 30 - July 3, 2009, Swansea, Wales, United Kingdom

Sat-Race 2008

• [ Youssef Hamadi , S. Jabbour and L. Sais] ManySAT1.0, gold medal, SAT Race 2008 (Parallel solvers category)

Best Paper Award

• [ Youssef Hamadi , Saïd Jabbour, and Lakhdar Saïs] Learning for Dynamic Subsumption. Proceedings of the 21th IEEE International Conference on Tools with Artificial Intelligence (ICTAI-09), 2009, (Best Paper Award)

---

Publications

Book chapter

• [ Youssef Hamadi , Saïd Jabbour, and L. Saïs], Control-based clause sharing in Parallel SAT, in "Complex Networks across the Natural and Technological Sciences", Eds. Maria Fox, Des Higham, Gian Luca Oppo and Ernesto Estrada, Springer 2010, to appear.

International Journals

• [ Youssef Hamadi , Saïd Jabbour, and Lakhdar Saïs] Learning in SAT , in in A Quarterly Journal of Operations Research 4OR, 2010, (invited survey)
• [ Youssef Hamadi , Saïd Jabbour, and Lakhdar Saïs] Learning for Dynamic Subsumption, in International Journal on Artificial Intelligence Tools ( IJAIT ), 2010 (invited paper).
• [Saïd Jabbour] Learning for dynamic assignments reordering, in International Journal on Artificial Intelligence Tools ( IJAIT), 2010, (invited paper).
• [ Youssef Hamadi , Saïd Jabbour, and Lakhdar Saïs], ManySAT: a new Parallel SAT solver, In Journal of Satisfiability Boolean Modeling and Computation, (JSAT), special issue on Parallel SAT solving, 2009, (PDF)
• [ Gilles Audemard , Saïd Jabbour, and Lakhdar Saïs] Graph-based SAT representation : a new perspective. In Journal of Algorithms in Logic, Informatics and Cognition (JALIC), 2008.

International Conferences

• [ Long Guo, Youssef Hamadi , Saïd Jabbour and Lakhdar Saïs] Diversification and Intensification in Parallel SAT Solving, in 16th International Conference on Principles and Practices of Constraint Programming (CP-10), St Andrews, Scotland, 2010 (to appear)
• [Saïd Jabbour and Lakhdar Saïs] Model-based elimination of symmetries in quantified boolean formulas, in Cinquième Conférence Internationale en Recherche Opérationnelle (CIRO-10), Marrakech, Morocco, 2010
• [ Youssef Hamadi , Saïd Jabbour, and Lakhdar Saïs] Learning for Dynamic Subsumption, in proceedings of the 21th IEEE International Conference on Tools with Artificial Intelligence (ICTAI-09), pages 328-335, 2009, (Best Paper Award) (PDF)
• [Saïd Jabbour] Learning for Dynamic Assignments Reordering, in proceedings of the 21th IEEE International Conference on Tools with Artificial Intelligence (ICTAI-09), pages 336-343, 2009, (PDF)
• [ Youssef Hamadi , Saïd Jabbour, and Lakhdar Saïs] Control-based clause sharing in Parallel SAT solving, in twenty-first International Joint Conference on Artificial Intelligence (IJCAI-09), Pasadena, California, pages 499-504, 2009, (PDF)
• [ Gilles Audemard , Lucas Bordeaux, Youssef Hamadi , Saïd Jabbour, and Lakhdar Saïs], A Generalized Framework for Conflict Analysis, in 11th International Conference on Theory and Applications of Satisfiability Testing (SAT-08), H. Kleine Büning and X. Zhao (Eds.), LNCS 4996, pages 21-27, Guangzhou, China, 2008.
• [ Gilles Audemard , Saïd Jabbour, and Lakhdar Saïs], Symmetry breaking in quantified boolean formulae, in International Joint Conference on Artificial Intelligence (IJCAI-07), pages 2262-2267, Hyderabad, India, 2007, (PDF)

International Workshops

• [ Gilles Audemard , Saïd Jabbour, Lakhdar Saïs], Efficient Symmetry breaking Predicates for quantified boolean formulae, in Proceedings of the International Workshop on Symmetry and Constraint Satisfaction Problems (SymCon-07) - Affiliated to CP, pages 14--21, Povidence, USA, 2007, (PDF)
• [ Gilles Audemard , Saïd Jabbour, Lakhdar Saïs], Using SAT-Graph representation to derive hard SAT instances. In Proceedings of the 14th Intl. Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion (RCRA-07), Roma, 2007, (PDF)

National Conferences

• [ Youssef Hamadi , Saïd Jabbour, et Lakhdar Saïs], Subsumption dirigée par l'analyse de conflits, dans les actes des Journées Francophones de Programmation par Contraintes (JFPC-09), Orleans, France, 2009, (PDF)
• [ Youssef Hamadi , Saïd Jabbour, et Lakhdar Saïs], Réordonnancement dynamique basé sur l'apprentissage, dans les actes des Journées Francophones de Programmation par Contraintes (JFPC-09), Orleans, France, 2009, (PDF)
• [ Gilles Audemard , Lucas Bordeaux, Youssef Hamadi , Saïd Jabbour, et Lakhdar Saïs], Un cadre général pour l'analyse des conflits, dans les actes des quatrièmes Journées Francophones de Programmation par Contraintes (JFPC-08), pages 267--276, Nantes, France, 2008, (PDF)
• [Saïd Jabbour], Représentation SAT-graph : une nouvelle perspective . Dans les actes des Journées d'Intelligence Artificielle Fondamentale (JAIF-07), 2-3, pages 44--58, Grenoble, France 2007, (PDF)
• [ Gilles Audemard , Saïd Jabbour, Lakhdar Saïs], Exploitation des symétries dans les formules booléennes quantifiées. Dans les Journées Francophones de la Programmation par Contraintes (JFPC-06), pages 15-24. Nîmes, France 2006, (PDF)

Technical Reports

• [ Youssef Hamadi , Saïd Jabbour, et Lakhdar Saïs] Learning from sucesses, technical report CRIL february, 2009.
• [ Youssef Hamadi , Saïd Jabbour, et Lakhdar Saïs] Control-based clause sharing in parallel SAT solving, technical report CRIL, january 2009.
• [ Gilles Audemard , Lucas Bordeaux, Youssef Hamadi , Saïd Jabbour, et Lakhdar Saïs] Generalized Framework for Conflict Analysis, technical report Microsoft Research, MSR-TR-2008-3, Fé́vrier 2008.

---

Ressources

Some tools developped during my research, availible for download

• ManySAT

  Description :

  For more information about our parallel SAT solver ManySAT, please go to this page: (ManySAT Solver)

• LySAT

  Description :

  LySAT a sequential solver based on Minisat2.0.

  Download the source code lysat.tgz

• sbp4QBF

  Description :

  Tool to remove symmetries in QBFs. Based on the approach proposed in the paper IJCAI'2007. This algorithm allows to translate a QBF F with symmetries to a new QBF F' asymmetric.

  Download the source code sbp4qbf.tgz

• mQSBP

  Description :

  an algorithm for the generation of pre-models from a symmetric QBF.

  Download the source code mqsbf.tgz

---

Teaching Activities

2008 - 2009

• algorithmic
• Data structures
• Web Programming
• Network
• Assembly language

2007 - 2008

• xHTML - CSS
• Algorithmic

2006 - 2007

• Algorithmic (Pascal language)
• Internet & Computer Science Certificate

---

Links

• ManySAT home page
• Inria-Microsoft Research joint centre
• CRIL Lens Computer Science Research Centre
• SAT Live a forum about everything you would want to know about SAT.
• sat competition official web site of SAT competition and results of the last years

---