Breaking the Dependency Chaos: A Constraint-Driven Python Dependency Resolution Strategy with Selective LLM Imputation

TL;DR

This paper introduces SMT-LLM, a hybrid Python dependency resolution system that combines formal constraint solving with LLM-based inference, significantly improving speed and accuracy over previous LLM-only approaches.

Contribution

SMT-LLM replaces LLM-only guessing with formal constraint solving, integrating static analysis, metadata inference, and SMT solving for more reliable dependency resolution.

Findings

Resolves 83.6% of snippets on HG2.9K benchmark, outperforming PLLM's 54.8%.

Reduces median resolution time from 151.5 s to 23.9 s, 6.3x faster.

Lowers average LLM calls per snippet from 24.9 to 2.26, 11x fewer.

Abstract

Dependency resolution is the task of selecting package versions that can be installed together without conflicts. It accounts for a significant share of build failures in modern software projects. In the Python ecosystem, this task is especially challenging due to Python 2/3 incompatibilities, deprecated packages, and widespread missing metadata. Recent work, such as PLLM, tackles this problem by using large language models (LLMs) to infer Python and package versions from code and iteratively repairing them based on build errors. We present SMT-LLM, a hybrid system that replaces LLM-only version guessing with formal constraint solving. SMT-LLM uses deterministic import extraction and Python version detection via abstract syntax tree (AST) analysis, the vermin tool to infer minimum Python versions, and a five-tier import-to-package resolver that queries PyPI before any LLM call. We construct a constraint graph from PyPI metadata and LLM-imputed dependencies for packages with missing metadata, then solve for consistent version assignments using a Z3 satisfiability modulo theories (SMT) solver. On the HG2.9K benchmark using Gemma2:9B (10 GB VRAM), SMT-LLM resolves 83.6% of snippets compared to PLLM's 54.8%, while reducing median resolution time from 151.5 s to 23.9 s (6.3x faster) and average LLM calls from ~24.9 to 2.26 per snippet (11x reduction).