Xing Zhao, Yixin Chen, Weixiong Zhang, and Ruoyun Huang


MaxPlan is an automated optimal propositional based on a satisfiability (SAT) formulation of STRIPS planning. The key innovation of MaxPlan is its use of the long distance mutual exclusion (londex), a novel generalization of the classic mutual exclusion (mutex). Based on a multi-valued domain formulation, londex provides much stronger space pruning than mutex since it can capture constraints relating actions not only at the same time step but also across multiple time steps. Several other novel techniques, including backward level reduction, accumulative learning of clauses, and SAT constraint partitioning, are also developed to further improve the search efficiency for both satisfiability solving and unsatisfiability proving.

Winner of the 1st Prize, Optimal Planning Track, Deterministic Part of the 5th International Planning Competition (IPC5), 2006

Propositional Domains (1st/2nd Places) 0/1 1/1 3/2 3/2 0/3
Temporal Domains (1st/2nd Places) 2/0
The plots of the performance of all competing planners in the deterministic track of IPC5 can be found here. An archive with all results can be found here. You can download all the domains in IPC5 from here.

Software Download

      Source code

        32-bit executable for Linux

        64-bit executable for Linux

Example command:
         maxplan -path domain_path -problem strips_problem -cgproblem adl_problem -domain strips_domain -cgdomain adl_domain -timeout 1800 -solver minisat

This research is supported by funds from the Washington University in St. Louis, an Early Career Young Investigator Award from the Department of Energy, and National Science Foundation Grant IIS-0535257.


For questions or bug report, please contact or
Last updated on Nov 30, 2006