ParaQuantumSAT: um algoritmo SAT solver distribuído

Abstract

The SAT problem is a classic and well known problem, been the first proved NP-complete. For its importance, since many equally NP-complete problems can be solved through reduction to the SAT problem, the study of techniques and algorithms for its solution is always a current issue of research. One way of speed up the achievement of a solution is through parallelism. Parallel computing is a critical study field, since the current speed of processing of computers grows with the parallelisation of processors, been one of the main challenges of the field the building of efficient parallel algorithms to solve classical computing problems. This work intends to develop a parallel SAT solver algorithm, using as base a sequential SAT solver algorithm.

O problema SAT é um problema clássico e bem conhecido, sendo o primeiro provado ser NP-completo . Por sua importância, já que diversos problemas igualmente NP-completo podem ser solucionados via redução ao problema SAT, o estudo de técnicas e algoritmos para a sua solução é sempre um tema atual de pesquisa. Uma forma de buscar acelerar a obtenção da solução é através de paralelismo. Computação paralela é uma área de estudo crítica, visto que hoje a capacidade de processamento dos computadores cresce com a paralelização dos processadores, sendo um dos principais desafios para a área a construção de algoritmos paralelos eficientes para resolver problemas clássicos de computação. Este trabalho se propõe a desenvolver um algoritmo SAT solver paralelo, tendo como base um algoritmo SAT solver sequencial.