Representação AIG como formato de entrada para o LIAMFSAT

Abstract

A Satisfatibilidade Booleana (SAT) é uma abordagem amplamente utilizada para verificação de software e hardware. Existem diversos resolvedores voltados para a resolução do problema de satisfatibilidade baseados no algoritmo Davis-Putnam-Logemann-Loveland (DPLL) e precisam que a fórmula esteja na Forma Normal Conjuntiva (CNF). Porém, muitos problemas não se encontram na representação CNF e então é necessária uma abordagem diferente para a resolução destes problemas. Os resolvedores não-clausais são voltados para a resolução de problemas que não se encontram na representação CNF, isto é, se encontram na representação não-clausal. Resolvedores não-clausais possuem diferentes abordagens, desde a conversão da fórmula não-clausal para a representação CNF à atuação diretamente na fórmula. Entretanto, a conversão para CNF pode ocasionar na perda considerável de informações sobre a estrutura do problema. Portanto, o objetivo deste trabalho consiste em um novo formato de entrada no resolvedor não-clausal LIAMFSAT, em que a abordagem utilizada foi a implementação da representação Grafo AND-Inversor (AIG), além de melhorias no resolvedor de modo a de facilitar trabalhos futuros.