O problema da Satisfatibilidade Probabilística (PSAT) é um problema na classe de complexidade dos problemas NP-completos que requer a aplicação conjunta de raciocínio dedutivo e probabilístico. Este problema consiste de uma atribuição de probabilidades ao um conjunto de fórmulas proposicionais, e sua solução é uma decisão sobre a consistência desta atribuição.
A formulação original de PSAT é atribuída a George Boole (1854). Desde então, o problema foi independentemente redescoberto diversas vezes, até ser introduzido à comunidade de Ciência da Computação e Inteligência Artificial por Nilsson (1986) e ser provado sua pertinência à classe NP-completo, mesmo para os casos em que o problema da satisfatibilidade clássica (SAT) é sabidamente polinomial. Nilsson chegou até a afirmar que se trata de um problema "de dificuldade muito alta" (1993).
Avanços recentes na teoria de PSAT mostraram que ele apresenta um comportamento de "Transição de Fase", ou seja, existem instâncias de PSAT de tamanho considerável que podem ser eficientemente resolvidas. Dois algoritmos foram propostas que apresentam este tipo de comportamento: uma redução polinomial de PSAT em SAT e uma mistura de técnicas de programação linear com SAT e geração de colunas.
Este projeto apresenta implementações destas duas técnicas.
Para maiores informações, visite a página do projeto: http://ccsl.ime.usp.br/psat