Este trabalho estuda o problema da Satisfazibilidade Probabilística (PSAT), revendo a sua solução via programação linear, além de propor novos algoritmos para resolvê-lo através da redução ao SAT. Construímos uma redução polinomial do PSAT para o SAT, chamada de Redução Canônica, codificando operações da aritmética racional em bits, como variáveis lógicas. Analisamos a complexidade computacional dessa redução e propomos uma Redução Canônica de Precisão Limitada para contornar tal complexidade. Apresentamos uma Redução de Turing do PSAT ao SAT, baseada no algoritmo Simplex e na Forma Normal Atômica que introduzimos. Sugerimos modificações em tal redução em busca de eficiência computacional. Por fim, implementamos essas reduções a m de investigar o perl de complexidade do PSAT, observamos o fenômeno de transição de fase e discutimos as condições para sua detecção.

This work studies the Probabilistic Satisfiability problem (PSAT), reviewing its solution through linear programming, and proposing new algorithms to solve it. We construct a polynomial many-to-one reduction from PSAT to SAT, called Canonical Reduction, codifying rational arithmetic operations into bits, as logical variables. We analyze the computational complexity of this reduction and we propose a Limited Precision Canonical Reduction to reduce such complexity. We present a Turing Reduction from PSAT to SAT, based on the Simplex algorithm and the Atomic Normal Form we introduced. We suggest modifications in such reduction looking for computational eficiency. Finally, we implement these reductions in order to investigate the complexity profile of PSAT, the phase transition phenomenom is observed and the conditions for its detection are discussed.