AI Planning / Optimization
A rigorous comparison of Z3, Gurobi, and solver-free LLM reasoning on constrained, real-data ski trip planning.
View repository1,009
ski resorts
15
benchmark queries
87.5%
Z3 constraint score
The benchmark asks a practical question: when a natural-language planning problem contains hard budgets, destinations, equipment, transport, and feasibility constraints, is an LLM alone enough? It compares pure language-model reasoning with two formally grounded planners over real ski-resort and rental data.
Planning responses can look convincing while silently violating budgets or omitting required services. The evaluation therefore needed to measure more than fluency: feasibility, hard-constraint satisfaction, commonsense consistency, optimality, repair quality, runtime, and cost all had to be scored.
Across fifteen queries and four difficulty bands, the reported results show a clear gap between plausible text and verified plans: Z3 reached 87.5% constraint satisfaction versus 16.7% for the pure LLM baseline, while Gurobi delivered the fastest average runtime in the headline comparison.
Technical approach
Parse natural-language requirements into destinations, duration, party size, budget, rentals, and slope preferences.
Run equivalent planning tasks through pure LLM, Z3 SMT, and Gurobi optimization pipelines.
Aggregate pass rate, hard and commonsense constraints, optimality, repair success, runtime, and cost metrics.