Selected Publications

SAT provers are powerful tools for solving real-sized logic problems, but using them requires solid programming knowledge and may be seen w.r.t. logic like assembly language w.r.t. programming. Something like a high level language was missing to ease various users to take benefit of these tools. TouIST aims at filling this gap. It is devoted to propositional logic and its main features are 1) to offer a high-level logic langage for expressing succintly complex formulas (e.g. formulas describing Sudoku rules, planification problems, …) and 2) to find models to these formulas by using the adequate powerful prover, which the user has no need to know about. It consists in a friendly interface that offers several syntactic facilities and which is connected with some sufficiently powerful provers allowing to automatically solve big instances of difficult problems (such as time-tables or Sudokus). It can interact with various provers: pure SAT solver but also SMT provers (SAT modulo theories - like linear theory of reals, etc) and thus may also be used by beginners for experiencing with pure propositional problems up to graduate students or even researchers for solving planification problems involving big sets of fluents and numerical constraints on them.
In TTL, 2015.

Publications

Most publications are available on the lab’s publications page.

. TouIST again... (Formalisez et résolvez facilement des problèmes avec des solveurs SAT, SMT et QBF). In IAF, 2017.

Details PDF Code Project

. La logique facile avec TouIST (poster). In JFPDA, 2017.

Details Code Project Poster

. Optimization of Dictionaries Structured as Convolutional Trees for Sparse Image Representation - Master’s Thesis. , 2016.

Details PDF

. La logique facile avec TouIST (formalisez et résolvez facilement des problèmes du monde réel). In IAF, 2015.

Details PDF Code Project

. Twist your logic with TouIST. In TTL, 2015.

Details PDF Code Project

Recent & Upcoming Talks

Presentation of the master's thesis work

Oct 6, 2016, Talk at the Information, Signal, Image and ViSion (ISIS) group meeting

Recent Posts

Projects

Minor contributions to open-source software

  • boost graph is a part of the large Boost C++ library. I mainly contributed through bug fixes to max flow algorithms.
  • gitlab is a competitor to Github; I proposed multiple bug fixes (as merge requests) to enhance the referencing behavior in issue tickets.

Projects contributed

TouIST

A friendly language for propositional logic and more

Logistique de crise et aide humanitaire (fr)

Compared study of two routing methods for use in humanitarian disaster

Teaching

I am a teaching instructor for the following courses at University Toulouse 3:

2016 (Université Toulouse 3 - Paul Sabatier)

  • Algorithms 1 (L1, all students): learn the basics of algorithmics using a simple programmning language (python) during 14 hours of practical work. I “taught” this course to chemists, physicists, mathematicians and computer scientists. Total: 42h.
  • Logic 1 (L2, Computer Science students): during 6 hours of pratical work, the students learn how to solve problems using propositional logic using TouIST. Total: 12h.
  • System 1 (L2, Computer Science students): during 12h of practical work, the students learn how to use and script using the Bourne Shell as well as many standard GNU/Linux utilities.

2017 (Université Toulouse 3 - Paul Sabatier)

  • Algorithms 1 (L1, students of parcours speciaux): same as previous year.
  • Language theory and compilation (M1, Computer Science students): in this really dense 8-hours pratical work, students must implement a compiler for the Karel language in OCaml, using the ocamlyacc or menhir parser generator that compiles to something close to assembly (quadruplets). As languages and compilers are the basis of any developper, this practical session give the students a good insight to the problems and complexity of any programming language. Total: 12h.
  • Advanced Algorithms (M1, Computer Science students): in this 6-hours long practical work, the students design, implement and prove the complexity of alternate versions of well-known algorithms (binary heap, quick sort); students are also shown linear programming, flow algorithms as well as global optimization. Total: 12h.

Contact