openSUSE:Libzypp satsolver 基本原理

Libzypp> Sat 求解器

本文介绍了 ZYpp 中使用的 SAT 求解器的基本概念。

以下内容基于 Michael Schröder 在 2008 年 FOSDEM 上发表的演示文稿。

SAT 问题

SAT：布尔可满足性问题

找到一个布尔表达式（与/或/非）中所有变量的真/假赋值，使其为真。NP 完全

归一化

(a | b | c) & (d | e | f) ... = TRUE

这些 (...) 项称为规则，由文字 a、b、c 组成，也可以被否定：-a

示例

(a | b | c) & (-c) & (-a | c) = TRUE

解：a = FALSE，b = TRUE，c = FALSE

SAT 的优势

研究充分的问题
- 许多示例求解器可用 (chaff, minisat...)
速度非常快
- 软件包求解的复杂度与其他使用 SAT 求解器的领域相比非常低
没有复杂的算法
- 求解只需要几百行代码
可理解的建议
- 求解器计算了问题无法解决的原因

从依赖关系到规则

需要：软件包依赖关系

A requires B provided by B1, B2, B3
Rule: (-A | B1 | B2 | B3)

“要么 A 未安装，要么 B1、B2、B3 中的一个已安装”

冲突：软件包依赖关系

A conflicts with B provided by B1, B2, B3
3 Rules: (-A | -B1), (-A | -B2), (-A | -B3)

“要么 A 未安装，要么 B1 未安装”

替代：软件包依赖关系

treated as conflicts

求解器算法

单元传播

如果所有文字都为 FALSE，则规则称为单元
如果规则是单元，则剩余的文字可以设置为 TRUE 示例

(a | b | c) & (-c) & (-a | c) = TRUE
c is FALSE     (unary rule)
(-a | c) is unit → -a is TRUE, a is FALSE
(a | b | c) is unit → b is TRUE

算法

自由选择：找到一些未决定的变量，分配 TRUE 或 FALSE
传播所有单元规则
重复直到所有变量都被决定

单元传播与依赖关系

需要规则(-A | B1 | B2 | B3)

A、B1、B2 为 FALSE → B3 必须为 TRUE
- “如果 A 已安装，并且所需依赖项的所有提供者（一个）都无法安装，则剩余的提供者必须安装”
- → 将软件包添加到安装集合
B1、B2、B3 为 FALSE → A 必须为 FALSE
- “如果所需依赖项的任何提供者都无法安装，则所需的软件包无法安装”
- → 将软件包添加到冲突/删除集合

冲突规则(-A | -B1)

A 为 TRUE → B1 必须为 FALSE，反之亦然

矛盾

单元传播可能导致矛盾
这意味着一个文字必须同时为 TRUE 和 FALSE
示例

 (-a | b) & (-a | c) & (-b | -c)

如果求解器将 a 设置为 TRUE → b、c 为 TRUE，c 为 FALSE！

从导致矛盾的规则中学习新规则
- → 学习的规则是 (-a)
- 撤销上次自由分配并继续求解
- 如果没有可撤销的，则问题无法解决

1996 年在 GRASP 求解器中首次实现。

处理自由选择

在这里您可以影响解决方案的质量

尝试保持软件包已安装
最小化要安装的软件包数量

算法

如果软件包之前已安装并且不在冲突集中，则安装它
如果规则不是 TRUE，但所有否定文字都为 FALSE，则选择未决定的正文字符的最佳字符并安装相应的软件包
(-A | B1 | B2) A TRUE → 选择 B1 或 B2
不要安装任何其他软件包（即，将所有未决定的变量设置为 FALSE）

系统策略

策略规则定义了如何处理已安装的软件包

不得卸载或降级
不得更改架构
不得更改供应商

规则格式

(A | A2 | A3 | A4)

A2/A3/A4 是允许的更新候选者（相同的名称和较新的版本或具有匹配的 Obsoletes：依赖项的软件包）

报告冲突

如果问题最终无法解决，则求解器算法将返回导致冲突的规则集。

由于没有 rpm 的系统是无冲突的，因此返回的规则集必须包含至少一个作业规则或策略规则。

可能的解决方案是删除其中一个规则，即删除一个作业（不要尝试安装软件包“foo”）或一个策略规则（允许卸载软件包“bar”）

优势：用户可以理解这些规则！

结论

使用 SAT 求解器算法解决了旧求解器所遇到的许多问题

速度：快几个数量级
可靠的结果
可扩展性：实现复杂的依赖关系很容易
合理的错误报告

我们还在开发一种新的存储库格式，可以更快地处理新的基于字典的 SOLV 格式。

参见

SAT 求解器内部原理

(-A)	无法安装软件包 A
	没有提供需求，错误的架构，...
	删除请求（作业规则）
(A)	必须安装软件包 A
	安装请求（作业规则）