Conferencia Jesús Giraldez Crú (Instituto de Investigación en Inteligencia Artificial (IIIA), Consejo Superior de Investigaciones Científicas. CSIC): “Beyond the Structure of SAT Formulas: Experiences of a PhD in Computer Science”.

In this talk, we summarize the main experiences of achieving a PhD in Computer Science. In a non-exhaustive list, we review some basic components of a pre-doctoral research, as the scheduling of the tasks, the search of bibliography or the publication of results, among others. In parallel, we summarize the main works in the field of this research, which is the Boolean Satisfiability problem (SAT) and its applications in real-world domains. SAT is one of the most studied problems in Computer Science since it is the first known NP-complete problem. However, besides its complexity, it is extensively used to solve practical applications (such as planning, scheduling or formal verification, among others). Modern SAT solvers have experienced a remarkable progress on solving these industrial (or real-world) SAT instances. Its success relies on the combination of some techniques, as conflict analysis, clause learning, non chronological backtracking, activity-based heuristics, lazy-data structures or rapid restarts.

Date: 25 June 2015.