Usando Redes de Petri e Resolvedores ISCAS para Tratar Planejamento como Satisfatibilidade - Montaño, Razer; Castilho, Marcos; Silva, Fabiano; Künzle, Luis (Anais do Encontro Nacional de Inteligência Artificial e Computacional (ENIAC); 2011: Anais do VIII Encontro Nacional de Inteligência Artificial, 2011)
Este trabalho apresenta uma abordagem para resolver o problema de planejamento clássico em IA como um problema de satisfatibilidade não clausal. Uma instância SAT em formato ISCAS é gerada pela conversão do problema de planejamento tendo como base uma rede de Petri na qual o problema de alcançabilidade de sub-marcação deve ser resolvido. A instância ISCAS é então resolvida usando-se resolvedores SAT não-clausais conhecidos.