openSUSE:Libzypp satsolver
SAT求解器库是适用于Linux的最强大的软件包依赖关系求解器和仓库存储系统。
依赖关系求解
求解依赖关系是Linux上任何软件包管理应用程序的核心功能。
依赖关系用于在多个软件元素之间划分和共享功能。
Linux（和Unix）遵循两种基本概念来实现分治算法——将一个大问题分解成更小、更易于管理的问题。
- 让每个程序做好一件事。详情请参见Unix哲学的基本原则。
- 使用共享库来共享实现并节省磁盘和内存空间
每个软件包通过依赖关系表达了它向他人提供的功能以及它从他人那里需要的那些功能。
依赖关系求解器的任务是在管理软件时检查和满足所有这些关系。
求解的基本法则
依赖关系求解器尝试在不进行用户干预的情况下解决依赖关系，基于两个基本规则
- 满足启动时给定的安装/删除请求
- 保持已安装系统的（依赖关系）一致性
由于求解器将每个软件包视为相同，这些规则有一些重大且有时意想不到的影响。一个损坏的依赖关系可能会导致删除许多软件包——结果系统仍然一致，但可能无法使用。
特性
使用可满足性求解器来计算软件包依赖关系。它基于将软件包依赖关系表示为布尔可满足性问题。
背景与信息
在openSUSE 11.0中出现的sat求解器实现基于两个主要但独立的模块
- 使用字典方法来存储和检索软件包和依赖关系信息。
- 使用可满足性，一个众所周知且经过研究的课题，来计算软件包依赖关系。
有关使用可满足性求解器解决软件包依赖关系的基础知识，请参见SAT求解器基础和SAT求解器内部原理以了解更多信息。
- 参见SAT求解器的历史。
- 参见可用的2008年FOSDEM演示。
开发者文档
版本：HEAD 开发者文档
版本：11.3 开发者文档
版本：11.2 开发者文档
参见
使用SAT求解器的工具和库。
外部链接
: