Large Language Models Can Solve Real-World Planning Rigorously with Formal Verification Tools (2025)

Abstract: Large Language Models (LLMs) struggle to directly generate correct plans for complex multi-constraint planning problems, even with self-verification and self-critique. For example, a U.S. domestic travel planning benchmark TravelPlanner was proposed in Xie et al. (2024), where the best LLM OpenAI o1-preview can only find viable travel plans with a 10% success rate given all needed information. In this work, we tackle this by proposing an LLM-based planning framework that formalizes and solves complex multi-constraint planning problems as constrained satisfiability problems, which are further consumed by sound and complete satisfiability solvers. We start with TravelPlanner as the primary use case and show that our framework achieves a success rate of 93.9% and is effective with diverse paraphrased prompts. More importantly, our framework has strong zero-shot generalizability, successfully handling unseen constraints in our newly created unseen international travel dataset and generalizing well to new fundamentally different domains. Moreover, when user input queries are infeasible, our framework can identify the unsatisfiable core, provide failure reasons, and offers personalized modification suggestions. We show that our framework can modify and solve for an average of 81.6% and 91.7% unsatisfiable queries from two datasets and prove with ablations that all key components of our framework are effective and necessary.

## introduction recent work has demonstrated that large language models (llms) @xcite @xcite , with abundant world knowledge, abilities to collect information via tools, and capabilities of reasoning, have significant potential in solving planning problems @xcite @xcite @xcite . however, modern llms are not well-suited for directly solving highly complex combinatorial optimization problems with multiple levels of constraints. this is because llms generate responses based on token probabilities derived from their training data and do not inherently possess the ability to perform rigorous logical or mathematical reasoning. to investigate the performance of llms on complex realistic multi-constraint problems, @xcite proposed a u.s. domestic travel planning benchmark, travelplanner, and showed that llms are not capable of handling this task and the best llm at the time, gpt-4, only achieves a 0.6% success rate. we test the strongest model of today, ope-nai o1-preview (o1p), with travelplanner and observed a pass rate of 10.0% even with access to pre-collected information. llm-modulo framework @xcite , a recent work that combines llms with external critics, verifiers, and humans, raises the pass rate to 20% with gpt-4-turbo and 65% with o1-preview, which is the best performance on travelplanner as of now. to tackle multi-constraint problems like travel planning, an alternative way is through constraintbased planning to formalize the problem as a constraint satisfaction problem (csp) @xcite , including boolean satisfiability problem (sat) @xcite and satisfiability modulo theory (smt) @xcite @xcite , and solve it with existing algorithm-based solvers @xcite @xcite . however, algorithm-based solvers usually have steep learning curves. as natural language queries have no fixed format, planners need to extract key information from input queries accurately to model the problem. crucially, even if the extracted information is correct, users must still modify inputs and query the tools repeatedly if their inputs are unsatisfiable. in short, llm-based and algorithm-based planning methods have complementary strengths: llms excel at parsing human input and interactions but struggle to rigorously solve complex planning problems with multiple constraints. in contrast, algorithm-based solvers are sound and complete when solving multi-constraint satisfiability problems but are incapable of handling dynamic, general, and sometimes ambiguous natural language requirements. can we design a framework that combines the merits of both paradigms and enables a strong, rigorous, and yet user-friendly planning experience for human users? motivated by this, in this paper, we propose a travel-planning framework that enables llms to process human queries and generate code to automatically utilize algorithm-based solvers, e.g., the smt solver, to formally formulate, solve, and reason over the planning problem. specifically, we take travel planning as the primary use case and provide llms with instruction steps and corresponding codes for using smt solver to solve the example travel planning problems. we find that, with only three examples in the prompt, the llm can effectively learn the pattern and generalize to new input queries. since a solver is called to solve the problem with all the constraints encoded, our method is guaranteed to generate a plan if it exists. notably, our method offers following features, including and beyond aforementioned advantages. ## dataset to access our framework's ability to 1) generalize to unseen constraints and 2) interactive plan repair for unsatisfiable queries, we propose a dataset, unsatchristmas, that introduces new constraints not included in travelplanner and contains 39 unsatisfiable queries under this setting. the queries in unsatchristmas aim to create an international travel plan for christmas week in 2023. we set cities in our dataset to be the top ten worldwide city destinations in 2019 1 and obtain attraction information from metabase foot_3 . we utilize google flights foot_4 to collect flight information from 12-24-2023 to 12-30-2023 for these ten cities. compared with travelplanner, we omit detailed information on transportation methods, restaurants, and accommodations but introduce detailed constraints regarding flights and attractions. as shown in ## experimental results we examine our framework on both travelplanner and unsatchristmas. we use gpt-4 @xcite with temperature 0 by default, and we also compare with claude 3 opus-20240229 (cla) and mistral-large (mis) with temperature 0 for satisfiable plan solving evaluation. we use z3 smt solver @xcite . since the solution space is prohibitive considering the combinatorial choices and a few queries have very limited feasible plans, we limit the smt solver's maximum runtime for each query to 30 minutes. please refer to appendix b for cost and runtime analysis. ## conclusion in this work, we propose a framework that enables llms to utilize an smt solver to formally formulate and solve complex realistic planning problems as constrained satisfiability problems. our framework generalizes to natural language query inputs, almost guarantees to deliver plans for satisfiable queries with a pass rate of 93.9%, and provides personalized suggestions to modify unsatisfiable queries. we prove our framework can handle diverse paraphrased prompts. we also show that our framework can generalize to unseen constraint types and new domains in a zero-shot manner.