Satplan (más conocido como Planning as Satisfiability) es un método de planificación automatizada . Convierte la instancia del problema de planificación en una instancia del problema de satisfacibilidad booleano , que luego se resuelve utilizando un método para establecer la satisfacibilidad como el algoritmo DPLL o WalkSAT .
Dada una instancia de problema en planificación, con un estado inicial dado, un conjunto dado de acciones, un objetivo y una longitud de horizonte, se genera una fórmula de modo que la fórmula sea satisfacible si y solo si existe un plan con la longitud de horizonte dada. Esto es similar a la simulación de máquinas de Turing con el problema de satisfacibilidad en la prueba del teorema de Cook . Se puede encontrar un plan probando la satisfacibilidad de las fórmulas para diferentes longitudes de horizonte. La forma más sencilla de hacer esto es recorrer las longitudes de horizonte secuencialmente, 0, 1, 2, y así sucesivamente.