Das Montanhas de Minas ao Oceano: Os Caminhos da Ciência para um Futuro Sustentável
20 a 25 de outubro de 2025
Trabalho 21093
| ISSN | 2237-9045 |
|---|---|
| Instituição | Universidade Federal de Viçosa |
| Nível | Graduação |
| Modalidade | Pesquisa |
| Área de conhecimento | Ciências Exatas e Tecnológicas |
| Área temática | Dimensões Econômicas: ODS9 |
| Setor | Departamento de Informática |
| Conclusão de bolsa | Não |
| Primeiro autor | André Luiz Feijó dos Santos |
| Orientador | LUIZ CARLOS DE ABREU ALBUQUERQUE |
| Outros membros | ANDRE GUSTAVO DOS SANTOS |
| Título | Verificação de Certificados de Modelo MILP |
| Resumo | Solvers de Programação Linear Inteira Mista (MILP) têm se tornado cada vez mais sofisticados, sendo aplicados em cenários críticos — nos quais erros não podem ser tolerados — como produtos de software financeiro e busca por contraexemplos. Diante da robustez das implementações comerciais modernas, é fundamental adotar uma postura cética quanto à corretude dos resultados obtidos. Embora a literatura sobre o tema ainda seja embrionária, avanços têm sido realizados na emissão de certificados — tanto de otimalidade quanto de inviabilidade — para soluções de instâncias MILP. O primeiro certificado genérico foi proposto pelo projeto VIPR 1.0, cujo formato representa o processo de otimização realizado pelo algoritmo Branch-and-Cut como um procedimento de inferência. Sendo assim, após a emissão do certificado, este precisa ser formalmente verificado para que haja uma prova de que a solução obtida está — de fato — correta. A literatura acerca deste problema indica que ainda existe um trade-off entre a segurança no processo de verificação — em função do ceticismo do algoritmo utilizado — e eficiência computacional. O objetivo desse trabalho é propor uma formulação segura e eficiente para a tarefa de verificação de certificados VIPR. Para isso, nesta pesquisa, este problema é formulado como um problema de satisfatibilidade, que pode ser resolvido com técnicas baseadas em Resolução, o que — portanto — garante uma implementação fundamentada em algoritmos já cientificamente consolidados. Atualmente, o verificador encontra-se em fase de desenvolvimento. Já sendo capaz de identificar a corretude das solução encontradas pelos solvers, está sendo ampliado para interpretar cada uma das regras de inferência contidas na prova. As principais contribuições deste trabalho incluem uma revisão da literatura acerca de certificação de programas inteiros; o estudo teórico de relações entre algoritmos de resolução de problemas de satisfatibilidade e Branch-and-Cut e a implementação de um verificador de certificados VIPR. Os resultados obtidos neste trabalho serão comparados aos de outros verificadores já propostos na literatura. |
| Palavras-chave | MILP, Certificados, Verificação Formal |
| Forma de apresentação..... | Painel |
| Link para apresentação | Painel |
|---|