TypiCal

In this talk we first 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. First, we propose an extended notion of implication graph containing additional arcs, called inverse arcs. These are obtained by taking into account the satisfied clauses of the formula, which are usually ignored in classical conflict analysis. Secondly, we present an original adaptation of conflict analysis for dynamic clauses subsumption. Our last contribution demonstrates that clause learning can be exploited at each step of the search tree, even if a conflict do not occurs. This last contribution aims to derive new but more powerful reasons leading to the implication of a given literal. For all these contributions, we discuss their possible integration to modern SAT solvers.