Sumários
8ª Aula
10 Abril 2017, 14:00 • João Marques Silva
A oitava aula iniciou o estudo de Satisfação Módulo Teorias (Satisfiability Modulo Theories, SMT). Foram apresentados exemplos de motivação incluindo os problemas de cooperative pathfinding, job-shop scheduling, e symbolic execution. A aula apresentou uma perspectiva de teorias de primeira ordem de interesse, incluindo igualdade com funções não interpretadas, aritmética linear e não linear, lógica de diferenças, bit vectors, entre outros. A aula descreveu também os algoritmos utilizados para resolver fórmulas SMT, os quais incluem as abordagens Eager e Lazy. A aula incluiu uma demonstração do resolvedor SMT Z3, e também da sua interface Python.
7ª Aula
3 Abril 2017, 14:00 • João Marques Silva
A sétima aula concluiu o estudo de problemas sobre-restringidos (overconstrained). A primeira parte da aula descreveu algoritmos para MaxSAT utilizandos minimum hitting sets (MHS). A segunda parte da aula cobriu a identificação de minimal unsatisfiable subsets (MUS), tendo sido descritos vários algoritmos elementares, e resumidos algoritmos avançados. Os algoritmos elementares estudados incluiram Deletion, Insertion e Dichotomic. A terceira parte da aula cobriu a indentificação de minimal correction subsets (MCS), tendo sido apresentados vários algoritmos elementares, e mencionados algorithms avançados. Os algoritmos elementares estudados incluiram linear search e Clause D. Foram também referidas optimizações práticas para identificação de MUSes e MCSes. A aula conclui com a apresentação da dualide por minimal hitting sets, entre MUSes e MCSes.