Planejamento como satisfatibilidade: uma abordagem não-clausal - Montaño, Razer; Silva, Fabiano; Castilho, Marcos; Künzle, Luis (Anais do Encontro Nacional de Inteligência Artificial e Computacional (ENIAC); 2007: Anais do VI Encontro Nacional de Inteligência Artificial, 2007)
A abordagem proposta consiste em resolver um problema de planejamento como alcançabilidade em redes de Petri. Inicialmente, traduz-se o problema em uma rede Petri acíclica. Uma fórmula SAT não-clausal é obtida a partir dos mutex entre as ações, explícitas na estrutura da rede. A resolução da fórmula SAT é feita através de Tableaux KE e corresponde a decidir todos os mutex na rede. Finalmente, resolver alcançabilidade nesta rede acíclica e sem conflitos é polinomial.