Saïd Jabbour (INRIA-Microsoft, Saclay)

In the first part of this talk (SAT) we give an introduction to modern SAT solving, and then we present several contributions to Conflict Driven Clause Learning (CDCL), which is one of the key components of modern SAT solvers. This includes an extended implication graph containing additional arcs, called inverse arcs. These arcs are obtained by taking into account the satisfied clauses of the formula, which are usually ignored in classical conflict analysis. We also prove that the scope of clause learning can be enlarged by addressing other problems such as dynamic simplification of boolean formula. The second part describes two contributions on symmetry breaking in the QBF context. Finally, we highlight our research program on both SAT and QBF.