Parallel Planning using a Lazy Clause Generation Solver

Reduction to a sequence of SAT problems has been a main approach for solving parallel planning problems for a long time. However, attempts at using constraint programming (CP) solvers for this purpose have witnessed relatively limited success. We show that existing CP formulations can deliver competitive results when a lazy clause generation solver (which is a hybrid of SAT and CP) is employed. This suggests promise for future cross-fertilization in SAT, CP, and AI planning.