SATyrus2: Compilando Especificações de Raciocínio Lógico

Apresenta-se, nesta dissertação, o SATyrus2, um compilador que se baseia no problema da Satisfabilidade booleana para traduzir modelos escritos sob a forma de restrições em problemas de programação linear inteira. SATish, uma linguagem declarativa de especificação, é fornecida como instrumento de modelagem para os problemas a serem resolvidos pelo SATyrus2. Por fim, a correção do compilador é avaliada por meio de testes realizados com a ARQ-PROP II, uma arquitetura capaz de realizar raciocínio proposicional por intermédio da aplicação do Princípio da Resolução.