O problema da Satisfatibilidade (também conhecido apenas por SAT) é um problema clássico na área de Ciência da Computação. Ele foi o primeiro problema descoberto a pertencer à classe dos problemas NP-completos e se constitui em decidir se é possível ou não que uma fórmula booleana seja verdadeira. Isso é, se existe uma atribuição de valores para as variáveis booleanas constituintes dessa fórmula que a satisfaça.
Uma extensão desse problema é o problema da Satisfatibilidade Probabilística (PSAT). Uma instância do PSAT é semelhante a uma instância do SAT, com a adição de que para cada variável booleana é associada uma probabilidade dela ser verdadeira ou não. Sua solução é uma decisão sobre a consistência desta atribuição de probabilidades para que a fórmula em questão seja satisfeita.
Glauber de Bona propôs dois algoritmos para solução desse problema [1] e desenvolveu dois softwares livres que os implementam (PSATtoSAT [2] e PsatColGen [3]) . Ambos os softwares são por sua vez baseados no uso do software livre zChaff [4] para a solução de instâncias do SAT necessárias para a solução da instância original do PSAT.
O objetivo desse trabalho é refinar o pacote de softwares livres disponíveis mencionados para resolver o PSAT, tanto para obter um melhor desempenho quanto para uma mais fácil distribuição do pacote.
Primeiramente será trocado o uso do zChaff pelo uso do MiniSat [5] (software livre que também resolve instâncias do SAT) e logo em seguida o próprio código do MiniSat usado para resolver o SAT será incluso tanto no PSATtoSAT quanto no PsatColGen para melhora de performance e para torná-los autocontidos.
| Atividade | Jun | Jul | Ago | Set | Out | Nov | Dez |
|---|---|---|---|---|---|---|---|
| Troca do zChaff pelo MiniSat (uso externo) no PsatColGen | x | ||||||
| Integração do código do MiniSat ao PsatColGen | x | x | |||||
| Início dos testes comparando as versões do PsatColGen | x | x | |||||
| Testes exaustivos em cima de todas as versões dos softwares | x | x | |||||
| Análise dos resultados obtidos e comparação de performance | x | x | |||||
| Finalização e atualização do código disponível | x | x | x | ||||
| Monografia | x | x | x | x | x | ||
| Pôster | x | ||||||
| Apresentação | x |