4ª Aula

13 Março 2017, 14:00 • João Marques Silva

A quarta aula apresentou uma perspectiva sobre os algoritmos para resolver o problema de decisão de lógica proposicional (i.e. o problema de satisfação proposicional, SAT). Foram descritos algoritmos baseados em procura local e em procura por retrocesso (DPLL). Posteriormente foi detalhada a organização dos algoritmos CDCL (Conflict-Driven Clause Learning), tendo sido apresentados os aspectos mais importantes: aprendizagem de cláusulas, retrocesso não cronológico, utilização do dominadores, estruturas de dados relaxadas, recomeços frequentes, minimização de cláusulas, entre outros. Foram ilustrados exemplos de utilização de SAT solvers em exemplos práticos, ilustrando as diferenças de desempenho entre as várias abordagens. Finalmente, foi apresentado um resumo das aplicações recentes de SAT solvers.