Dissertação

Machine learning of strategies for efficiently solving QBF with abstraction refinement EVALUATED

QFUN é um solver de Fórmulas Booleanas Quantificadas (QBFs) baseado no paradigma de Refinamento de Abstrações Guiado por Contra-exemplos (CEGAR), que utiliza aprendizagem automática para aprender estratégias para variáveis durante a resolução de QBFs. A aprendizagem automática de estratégias durante a resolução de QBFs é uma técnica recente, que cria novas possibilidades de melhoria da eficiência dos solvers. O nosso trabalho consistiu na pesquisa, desenvolvimento, implementação e avaliação de algoritmos de aprendizagem alternativos para o solver QFUN. Implementámos seis algoritmos alternativos para a aprendizagem do solver, e avaliámos experimentalmente a sua performance. Pudemos concluir que dois dos algoritmos melhoraram a performance de QFUN, enquanto dois outros têm uma performance semelhante ao algoritmo de aprendizagem original. Além disso, avaliámos a performance do solver, utilizando os diferentes algoritmos de aprendizagem, com famı́lias especı́ficas de QBFs e identificámos famı́lias para as quais esta abordagem é eficiente, simultaneamente analisando quais os algoritmos mais adequados para cada famı́lia. Concluimos, com base nos resultados experimentais, que a aprendizagem automática melhora consi- deravelmente a performance do solver, para algumas famı́lias de fórmulas.
fórmulas Booleanas quantificadas, aprendizagem automática, CEGAR

Julho 15, 2019, 14:0

Publicação

Obra sujeita a Direitos de Autor

Orientação

ORIENTADOR

Mikolas Janota

Departamento de Engenharia Informática (DEI)

Professor Auxiliar

ORIENTADOR

Carlos Manuel Costa Lourenço Caleiro

Departamento de Matemática (DM)

Professor Associado