Projeto de pesquisa, UFV
Verificação de Certificados de Modelos MILP
Descrição
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. 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 formato de certificado genérico foi proposto pelo projeto VIPR 1.0, registrando o processo de otimização do solver SCIP. Após a emissão do certificado, este precisa ser formalmente verificado. O objetivo desse trabalho é propor uma formulação segura e eficiente para a tarefa de verificação de certificados VIPR.
Palavras-chave
- MILP
- Certificados
- SMT
- Verificação Formal
Grupo de pesquisa
Algoritmos e Otimização Combinatória
Candidatar-se
A UFV não divulga o e-mail de cada coordenação nos dados abertos. Use a página do projeto no sistema de pesquisa da UFV (link acima) ou procure o departamento indicado.