Um método de pré-processamento de fórmulas SAT e pseudo-boolean baseado em técnicas de programação linear inteira mista

Abstract

Resumo: Ao longo da última década, resolvedores de Satisfatibilidade Booleana (SAT) e Programação Inteira Linear (ILP) melhoraram significativamente com a introdução de novos algoritmos, que permitiram o tratamento de um conjunto mais abrangente de problemas desafiadores e do mundo real, a exemplo, planejamento [39] e verificação de microprocessadores [66]. Existe, também, a representação pseudo-Booleana dentro do escopo de SAT, onde cada variável possui um coeficiente inteiro associado, e as restrições passam a ser desigualdades. A representação pseudo-Booleana é bastante rica e é possível modelar problemas reais facilmente utilizando essa abordagem. Apesar dessa representação ser ligeiramente diferente das representações tradicionais de SAT, ficando mais próxima da representação ILP, as técnicas utilizadas para resolver os problemas são bastante intercambiáveis, possibilitando o aproveitamento dos avanços de SAT nas últimas décadas. Resolvedores tradicionais falham em resolver diversos problemas por sua demanda por tempo de processamento, e por isso as comunidades têm buscado maneiras de pré-processar as fórmulas [25, 58, 50, 5] a fim de gerarem uma nova fórmula equisatisfatível e que demande menos tempo de processamento para serem resolvidas. Nesta tese, propomos e implementamos um método de pré-processamento de fórmulas pseudo-Booleanas, pseudo-Boolean Constraint Reduction - pBCR, utilizando técnicas da comunidade de pesquisa operacional no intuito de aplicar em fórmulas de diversos domínios de interesse da comunidade de SAT e pseudo-Boolean. Mostramos que a aplicação destas técnicas possui um tempo viável de processamento. Resultados experimentais foram feitos e analisados, permitindo mostrar que o tempo de pré-processamento mantém o tempo total, resolver a fórmula e pré-processar, viável na maioria dos casos. Aplicamos o método proposto sobre o problema da consolidação de máquinas virtuais. As fórmulas geradas por este estudo de caso foram usadas como parte do domínio de testes da competição de resolvedores pseudo-Booleanos de 2015.

Abstract: Over the last decade, Boolean Satisfiability (SAT) solver and Integer Linear Programming (ILP) have improved significantly with the introduction of new intelligent algorithms which allowed to solve more challenging and broader range of problems, for instance, planning [39] and microprocessor verification [66]. Inside the SAT scope, there is the pseudo-boolean representation, where each variable has an integer coeficient and restrictions becomes inequalities. The pseudo-Boolean representation is very rich and it is possible model real world problems easily using this approach. Although this representation is slightly different from traditional representations of SAT, being closer to ILP, the techniques used to solve problems are very interchangeable, enabling the possibility to use recent advances from SAT of the last decade. Traditional solvers fail to solve several problems for their processing demand, and both communities are in pursue of ways to pre-process the formulae [25, 58, 50, 5] in order to generate a new equisatisfiable formula that demands less processing time to be solved. A new pre-processor of pseudo-Boolean formulae has been implemented, named pseudo- Boolean Constraint Reduction - pBCR, using techniques from the operations research community to be used in domains of interest for the SAT and pseudo-Boolean communities. We show that the use of these techniques have viable processing time. Experimental results were run, analyzed and we have shown that the pre-processing time keeps the total time, to pre-process and solve the formula, viable in most cases. We applied the proposed method on the problem virtual machine consolidation. The generated formulae for this study are being used as a domain for the pseudo-Boolean competition of 2015.