SATyrus2: Compilando Especificações de Raciocínio Lógico
Autores
4779 |
Bruno França Monteiro
|
2131,131,162
|
4780 |
2131,131,162
|
|
4781 |
2131,131,162
|
Informações:
Publicações do PESC
Título
SATyrus2: Compilando Especificações de Raciocínio Lógico
Linha de pesquisa
Arquitetura e Sistemas Operacionais
Tipo de publicação
Dissertação de Mestrado
Número de registro
Data da defesa
30/3/2010
Resumo
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.
Abstract
In this work we present SATyrus2, a compiler that is based on the Boolean Satisfiability problem. SATyrus2 can compile models written in the form of restrictions in binary integer programming instances. Satish, a declarative programming language, is provided as a tool for modeling problems that can be solved by SATyrus2. Finally, ARQ-PROP II, a limited-depth propositional reasoner, is used to test the correctness of SATyrus2.
Arquivo