SMTpip：面向Python源码可执行性恢复的感知解释器的基于SMT的依赖冲突解决方法
SMTpip: Interpreter-Aware SMT-Based Dependency Conflict Resolution for Restoring Python Source-Code Executability
浏览论文内容
中文总结 AI 辅助
本文提出SMTpip，一种感知解释器的Python依赖冲突解决技术，通过将约束编码为SMT公式求解，实现比pip、Conda等工具更快的约束一致环境生成，提升Python源码可执行性恢复效率。
中文摘要 AI 辅助
软件开发者依赖包来复用现有功能，而非从零实现所有内容。Python开发者通常使用配置文件（如requirements.txt或pyproject.toml）提供包和解释器依赖。Python的包管理器（如pip）可根据配置文件中指定的依赖和解释器版本约束安装包。但Python依赖解决仍存在挑战：（1）不同包可能要求同一依赖的不兼容版本；（2）依赖可能要求与项目所用解释器不兼容的Python解释器版本，导致无法生成有效环境；（3）最流行的Python包管理器pip通过回溯解决冲突，反复尝试候选版本，却无法判断是否存在有效执行环境。为应对这些挑战，本文提出SMTpip，一种感知解释器的环境推断技术，用于提升Python源码制品的可执行性。SMTpip利用托管数百万包版本的Python包索引（PyPI）中存储的元数据构建依赖知识图谱，将配置文件中指定的包版本约束和解释器兼容性约束编码为可满足性模理论（SMT）公式。求解这些公式可识别出一组包版本和一个解释器版本，共同满足所有声明的约束。对来自开源Python项目的多个数据集的实证评估显示，SMTpip实现了显著的速度提升——相比pip快6.9倍，相比Conda快9.6倍，相比smartPip快3.2倍，相比PyEGo快4倍，且始终生成与约束一致的环境。
英文摘要
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.
