Utilize este link para identificar ou citar este item:
https://bdm.unb.br/handle/10483/33855
| Título: | Resolvendo fórmulas Horn mistas com um algoritmo 𝑂(20.5284×𝑁) |
| Autor(es): | Pinto, André Lucas de Sousa |
| Orientador(es): | Ribas, Bruno César |
| Assunto: | Lógica
Ciência da Computação
Inteligência artificial |
| Data de apresentação: | 5-Mai-2022 |
| Data de publicação: | 27-Fev-2023 |
| Referência: | PINTO, André Lucas de Sousa. Resolvendo fórmulas Horn mistas com um algoritmo 𝑂(20.5284×𝑁). 2022. 64 f., il. Trabalho de Conclusão de Curso (Bacharelado em Engenharia de Software) — Universidade de Brasília, Brasília, 2022. |
| Resumo: | A satisfatibilidade booleana é um problema que, dada uma expressão lógica, é decidido se existe algum conjunto de variáveis valoradas de modo a tornar a expressão verdadeira. Tal problema é de fundamental importância em áreas como ciência da computação, inteligência artificial e projetos de hardware. Embora satisfatibilidade booleana seja um problema NP-completo, um algoritmo de complexidade 𝑂(20.5284×𝑁 ) foi definido para resolver especificamente a classe de fórmulas Horn mistas utilizando algoritmos de geração de conjuntos independentes máximos. O objetivo deste trabalho é construir um resolvedor de satisfatibilidade para fórmulas Horn mistas e comparar seu desempenho com resolvedores atuais. As fórmulas Horn mistas são um conjunto de fórmulas compostas de uma parte Horn e uma parte na forma normal conjuntiva contendo no máximo duas cláusulas. |
| Abstract: | Boolean satisfiability is a problem that, given a logical expression, it decides whether there is some set of variables valued in order to make the expression true. Such a problem is of fundamental importance in areas such as computer science, artificial intelligence and hardware projects. Although Boolean satisfiability is an NP-complete problem, an algorithm of complexity 𝑂(20.5284×𝑁 ) was defined to specifically solve the class of mixed Horn formulas using algorithms for generating maximum independent sets. The objective of this work is to build a satisfiability solver for mixed Horn formulas and compare its performance with current solvers. Mixed Horn formulas are a set of formulas composed of a Horn part and a conjunctive normal form part containing at most two clauses. |
| Informações adicionais: | Trabalho de Conclusão de Curso (graduação) — Universidade de Brasília, Faculdade UnB Gama, Engenharia de Software, 2022. |
| Licença: | A concessão da licença deste item refere-se ao termo de autorização impresso assinado pelo autor que autoriza a Biblioteca Digital da Produção Intelectual Discente da Universidade de Brasília (BDM) a disponibilizar o trabalho de conclusão de curso por meio do sítio bdm.unb.br, com as seguintes condições: disponível sob Licença Creative Commons 4.0 International, que permite copiar, distribuir e transmitir o trabalho, desde que seja citado o autor e licenciante. Não permite o uso para fins comerciais nem a adaptação desta. |
| Aparece na Coleção: | Engenharia de Software
|
Todos os itens na BDM estão protegidos por copyright. Todos os direitos reservados.
