Sumários
6ª Aula
27 Março 2017, 14:00 • João Marques Silva
A sexta aula iniciou o estudo de problemas sobre-restringidos (overconstrained). Foram apresentados vários tipos de problemas relacionados com a análise de problemas sobre-restringidos: explicações minímas e minimais, e relaxações máximas a maximais. Foram apresentados dois problemas concretos, nomeadamente o problema de maximum satisfiability (MaxSAT) e o problema de minimum satisfiability (MinSAT). A aula estudou com maior detalhe o problema de MaxSAT. Foram apresentados vários exemplos de modelação, realçando aplicações práticas. Finalmente, foram estudados algoritmos baseados em resolução iterativa de restrições, procura branch-and-bound, e baseados em identificação iterativa de cores.
5ª Aula
20 Março 2017, 14:00 • João Marques Silva
A quinta aula desenvolveu um exemplo de solução do projecto 1. Esta solução foi disponibilizada aos alunos.
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.