Satplan (más conocido como Planificación como Satisfacción) es un método de planificación automatizada . Convierte la instancia del problema de planificación en una instancia del problema booleano de satisfacibilidad , 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 de acciones dado, una meta y una longitud de horizonte, se genera una fórmula de modo que la fórmula sea satisfactoria si y sólo si hay 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 demostración 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 del horizonte secuencialmente, 0, 1, 2, etc.