Search papers, labs, and topics across Lattice.
SMTpip introduces an interpreter-aware technique for resolving dependency conflicts in Python, addressing the limitations of traditional package managers like pip that rely on backtracking. By constructing a dependency knowledge graph and encoding constraints into Satisfiability Modulo Theories (SMT) formulas, SMTpip effectively identifies compatible package and interpreter versions that satisfy all specified requirements. Empirical evaluations demonstrate that SMTpip significantly outperforms existing solutions, achieving speedups of up to 9.6 times over Conda while ensuring consistent execution environments.
SMTpip resolves Python dependency conflicts 6.9 times faster than pip by leveraging SMT-based inference for interpreter-aware environment construction.
Software developers rely on packages to reuse existing functionality instead of implementing everything from scratch. Python developers commonly provide package and interpreter dependencies using configuration files, such as requirements.txt or setup.py. Package managers in Python, such as pip, can install packages according to dependency and interpreter version constraints specified in configuration files. However, Python dependency resolution remains challenging: (1) different packages may require incompatible versions of the same dependency; (2) dependencies may require a Python interpreter version that is incompatible with the interpreter used for the project, making a valid environment impossible; and (3) pip, the most popular Python package manager, resolves conflicts via backtracking, repeatedly trying candidate versions without knowing whether a valid execution environment exists or not. To address these challenges, we present SMTpip, an interpreter-aware environment inference technique for improving the executability of Python source-code artifacts. SMTpip constructs a dependency knowledge graph using metadata stored in the Python Package Index (PyPI) that hosts millions of package releases, encodes both package version constraints and interpreter compatibility constraints specified in configuration files into Satisfiability Modulo Theories (SMT) formulas. Solving these formulas identifies a set of package versions and an interpreter version that jointly satisfy all declared constraints. Empirical evaluation on multiple datasets from open-source Python projects shows that SMTpip achieves substantial speedups -- $6.9\times$ over pip, $9.6\times$ over Conda, $3.2\times$ over smartPip, and $4\times$ over PyEGo -- while consistently producing constraint-consistent environments.
