Plan de Satplan

Satplan (más conocido como Planning as Satisfiability) es un método para la planificación automatizada . ^{[ 1 ] [ 2 ]} Convierte la instancia del problema de planificación en una instancia del problema de satisfacibilidad booleana (SAT), que luego se resuelve utilizando un método para establecer la satisfacibilidad, como el algoritmo DPLL o WalkSAT .

El proceso codifica los elementos clave del problema de planificación —estado inicial, acciones disponibles, estado objetivo y longitud máxima del plan (longitud del horizonte)— en una fórmula lógica. Esta fórmula es satisfacible si y solo si existe una secuencia válida de acciones que transforma el estado inicial en el estado objetivo dentro del horizonte dado. Este concepto es similar al teorema de Cook , donde los cálculos de la máquina de Turing se representan como fórmulas SAT. ^{[ 3 ]}

Para encontrar un plan, Satplan prueba iterativamente fórmulas con horizontes temporales crecientes. Comienza con un horizonte de 0 (sin acciones) y lo incrementa gradualmente (1, 2, 3, etc.). Para cada horizonte, se genera una fórmula SAT correspondiente que es verificada por un solucionador SAT. Si es satisfacible, la salida del solucionador revela la secuencia de acciones. Si no lo es, el proceso continúa hasta encontrar un plan válido. Si bien este enfoque simple puede ser ineficiente, estrategias de búsqueda más avanzadas pueden mejorar el rendimiento, pero la idea fundamental sigue siendo la misma: reducir la planificación a la satisfacibilidad. ^{[ 4 ]}

• Plano de gráficos

• HA Kautz y B. Selman (1992). La planificación como satisfacibilidad . En Actas de la Décima Conferencia Europea sobre Inteligencia Artificial (ECAI'92) , páginas 359–363.
• HA Kautz y B. Selman (1996). Superando los límites: planificación, lógica proposicional y búsqueda estocástica . En Actas de la Decimotercera Conferencia Nacional sobre Inteligencia Artificial (AAAI'96) , páginas 1194–1201.
• J. Rintanen (2009). Planificación y SAT . En A. Biere, H. van Maaren, M. Heule y Toby Walsh, Eds., Manual de Satisfacibilidad , páginas 483–504, IOS Press . ISBN 978-1-58603-929-5.