PROVERBS -- Sistemas Booleanos Probabilísticos Super-restritos: ferramentas de raciocínio e aplicações

Resumo

A solução de problemas computacionais envolvendo objetos do mundo necessita conciliar modelos rigorosos com informações imperfeitas e flexíveis coletadas sobre o mundo. Assim, o método de solução deste tipo de problema deve ser capaz de lidar tanto com as rígidas asserções sobre o mundo quanto com o fluxo e informações cujo natureza é muito menos rígida. A capacidade de tratar de tal situação nos permitirá lidar com dispositivos computacionais inseridos num mundo em que, o fluxo de informações está constantemente mudando, de forma imprecisa e incerta.Este projeto estuda os problemas que se combinam restrições rígidas com restrições flexíveis envolvendo preferências, incertezas e exigências maleáveis. Neste trabalho, as restrições rígidas são representadas por conjuntos de fórmulas booleanas. As restrições flexíveis podem assumir a forma de pesos numéricos associados a algumas fórmulas booleanas. E a solução do problema trata de encontrar um conjunto de fórmulas que pode ser satisfeita de forma a maximizar o valor total associado às restrições satisfeitas. Esta abordagem é chamada de máxima satisfatibilidade (MaxSAT) para o problema de tratar de restrições rígidas e flexíveis. Outra maneira de modelar restrições flexíveis é associar probabilidades a algumas das fórmulas, caso em que a solução do conjunto total de restrições é um distribuição de probabilidade sobre os modelos que atendem às restrições rígidas, que também verifique as restrições flexíveis de probabilidade. Esta abordagem é chamada de satisfatibilidade probabilística (PSAT) para restrições rígidas e flexíveis.Em muitas situações, as técnicas de modelagem rígido-flexível de restrições booleanas podem levar a formulações super-restritivas, isto é, um conjunto de restrições para as quais nenhuma interpretação consistente é possível. Importantes aplicações podem ser modeladas por formulações super-restritivas de condições rígido-flexíveis em diversas áreas, dentre as quais serão exploradas neste projeto: segurança de informações, verificação de protocolos e planejamento, e linguística computacional.A natureza dessas restrições nos colocam no centro da classe de problemas computacionais intratáveis conhecida como NP-difíceis, para a qual nenhum algoritmo geral eficiente é conhecido, mas para o qual muitas instâncias de solução simples foram descobertas nos últimos anos. Acreditamos que uma fertilização cruzada entre essas duas abordagens pode levar a um progresso significativo no tratamento computacional de restrições rígido-flexíveis. Ao combinar a experiência de pesquisadores de alto nível em ambas abordagens, este projeto tem como objetivo principal a levar as técnicas e aplicações desta área a um novo patamar.Planejamos desenvolver vários algoritmos para lidar com problemas MaxSAT e PSAT, incluindo o tratamento de PSAT usando MaxSAT. Em seguida, planejamos aplicar essas técnicas na solução de formulações super-restritivas. Os programas desenvolvidos serão disponibilizados como software livre de código aberto. Vamos desenvolver aplicações destas técnicas e algoritmos abrangendo as áreas de segurança da informação, verificação de protocolos e linguística computacional .Este projeto apresenta o lado brasileiro de uma colaboração de pesquisa entre grupos de pesquisa com base em duas universidades em Portugal e no Brasil que visam estudar esses métodos e abordagens para explorar o problema de formulações probabilísticas super-restritivas. (AU)