PluSAT : um resolvedor SAT modular

Abstract

Este trabalho apresenta um novo resolvedor SAT nomeado PluSAT, um resolvedor com estrutura modular e extensível que possibilita que seus usuários possam modificar o seu comportamento usando plugins. A estrutura interna do resolvedor é baseada em resolvedores CDCL (Conflict-Driven Clause Learning), nossa interface de extensão possibilita a alteração do comportamento de etapas como: heurística de decisão, retrocessos, BCP (Boolean Constraint Propagation), reinícios e análise de conflitos. A estrutura do PluSAT procura oferecer aos desenvolvedores de resolvedores uma forma rápida para implementar esse tipo de solução, enquanto aqueles interessados em iniciar seus estudos podem trabalhar em cada componente separadamente, sem se preocupar com todo o fluxo de um resolvedor comum diminuindo assim a curva de aprendizado necessária para implementar um resolvedor na prática. Toda implementação deste resolvedor está disponibilizada de forma open source.