Aplicação de formulas não-clausais em planejamento com redes de Petri

Abstract

Resumo: Redes de Petri (RdP) podem ser usadas para modelar um problema de planejamento de maneira similar ao uso do grafo de planos. Porém, apesar da representação em RdP apresentar características interessantes para a modelagem, encontrar o plano efetivamente tem sido um problema difícil de se tratar computacionalmente. Isto requer normalmenter esolver o problema de Alcançabilidade em Redes de Petri (PSPACE-completo) com milhares/milhões de nodos. Neste trabalho investiga-se representações e algoritmos para SAT para resolução dos conflitos na rede que levariam à solução do problema de alcançabilidade. A obtenção da instância SAT é feita a partir da RdP e leva ao estudo de formas normais não-clausais e algoritmos eficientes para as fórmulas obtidas.

Abstract: Petri Nets (RdP) can be used to model planning problems in similar way to graph of plans. However, despite the representation in RdP presenting interesting characteristics for the modeling, effectively to find the plan has been a hard computational problem. This normally requires to decide the problem of Reachability in Petri Nets (PSPACE-complete) with thousands/millions of nodes. In this work, we investigate representations and algorithms for SAT for resolution of the conflicts in the net that would lead to the solution of the reachability problem. The SAT instance obtained is generated from the RdP and takes to the study of non-clausal normal forms and efficient algorithms for them.