openSUSE:Libzypp satsolver 内部机制

Libzypp> Sat 求解器

基础 - 内部机制 - 开发

本文档描述了 ZYpp 中使用的 SAT 求解器的内部概念，并解释了它如何通过简单的示例工作。

内部机制

池和源

规则

规则的定义

存在一些类型的规则

直接断言：例如 (A) = 安装 A；(-A) = 卸载 A

二元规则：例如 (!A|B) = A 需要 B

具有两个以上可能性的规则：(!A|B1|B2 ) = A 需要 B1 或 B2

一个规则包含一个单独的文字（称为 p）和一个指向文字数组的指针（称为 d）。以下是一些示例

p = 直接文字；始终小于 0 用于已安装的 rpm 规则

d，如果小于 0，则为直接文字，如果大于 0，则为 whatprovides 中的偏移量，如果等于 0，则规则为断言（仅查看 p）

安装：p > 0，d = 0 (A) 用户请求安装
卸载：p < 0，d = 0 (-A) 用户请求卸载
需要：p < 0，d > 0 (-A|B1|B2|...) d：<p 的需求提供者列表>
更新：p > 0，d > 0 (A|B1|B2|...) d：<可解 p 的更新列表>
冲突：p < 0，d < 0 (-A|-B) 冲突发布者为 p 或 d（二元规则）
无操作 ?: p = 0，d = 0 (null)（用作策略规则占位符）

规则数组

规则存储在一个数组中。此外，规则在数组中分组

涉及软件包的 rpm 规则

任务规则

已安装的可解规则（已安装规则）

弱规则（即，如果无法求解，则自动禁用的规则）

学习规则

大多数组都有定义的偏移量变量

solv->learntrules

solv->weakrules

solv->systemrules

solv->jobrules

此数组的长度由以下内容定义

solve->nrules

任务

任务存储在作业队列中。每个作业有两个元素

如何 :
- SOLVER_INSTALL_SOLVABLE
- SOLVER_ERASE_SOLVABLE
- SOLVER_INSTALL_SOLVABLE_NAME
- SOLVER_ERASE_SOLVABLE_NAME
- SOLVER_INSTALL_SOLVABLE_PROVIDES
- SOLVER_ERASE_SOLVABLE_PROVIDES
- SOLVER_INSTALL_SOLVABLE_UPDATE
内容 :
- 可解 ID 或
- 提供的字符串 ID 或
- 依赖项 ID

观察数组

观察数组将在求解器开始求解之前生成，并在求解器运行时更新。当相应的文字变为 False 时，观察会被触发。由于存在正文字和负文字，我们需要 nsolvables*2 个条目。每个条目都是通过所有相关规则的链接列表。

观察数组的构建方式取决于每个规则中的信息。规则有两个定义的观察点 (w1,w2)，具体取决于规则的类型

直接断言（不需要观察）（如果 d <0）--> d = 0，w1 = p，w2 = 0
二元规则：p = 第一个文字，d = 0，w2 = 第二个文字，w1 = p
其他：w1 = p，w2 = whatprovidesdata[d];
禁用规则：w1 = 0

(p 和 d 在规则定义章节中解释)

观察数组有 nsolvables*2 个条目，并且从中间寻址

middle-solvable：冲突的决策，偏移量指向规则的链接列表
middle+solvable：安装的决策：偏移量指向规则的链接列表

因此，索引是可解 ID（负数或正数），并且该值将是规则的相应观察点。对于每个规则，这些观察点将在观察数组中被考虑

 static void
 addwatches(Solver *solv, Rule *rule)
 {
   int nsolvables = solv->pool->nsolvables;
   rule->n1 = solv->watches[nsolvables + rule->w1];
   solv->watches[nsolvables + rule->w1] = rule - solv->rules;
   rule->n2 = solv->watches[nsolvables + rule->w2];
   solv->watches[nsolvables + rule->w2] = rule - solv->rules;
 }

在覆盖新的观察点之前，已定义的观察点将存储在规则的 n1 或 n2 中。

决策

决策存储在 3 个不同的队列/映射中。

decisionq

是可解 ID 的队列，反映了将要安装（正 ID）或将要删除（负 ID）的可解的状态。

此队列的长度存储在 decisionq.count 中。

decisionmap

索引是相关可解的 ID。该值反映了安装（正数）或冲突（负数）的决策级别。

decisionq_why

是与 decisionq 对应的规则 ID 的队列。此队列保存求解器做出决策的原因。原因是如果规则变为 unit，则为规则索引，或者为“0”。

该值为“0”如果

相关可解是 SYSTEMRESOLVABLE，它始终安装。
该决策仅是 rpm 规则断言。我们不为那些创建规则。
该决策是任意选择完成的。

此队列的长度存储在 decisionq_why.count 中。

SAT 求解器的工作原理

获得求解器工作原理的概述的最佳方法是通过简单的示例来解释它。

最佳情况（无问题）

环境

软件包	provides	requires	conflicts
A	a, foo		h
B	b, foo		g
C	c, foo		f
D	d, foo		e
E	e, bar		d
F	f, bar		c
G	g, bar		b
H	h, bar		a
Z		foo, bar

任务

软件包	action
A	install
B	install

构建规则

创建涉及作业的软件包的 rpm 规则

 Rule #1:
   !Z-1.0-1.noarch [11] (w1) Install.level1
   A-1.0-1.noarch [3] (w2) Install.level1
   B-1.0-1.noarch [4]
   C-1.0-1.noarch [5]
   D-1.0-1.noarch [6]
   next rules: 0 0
 Rule #2:
   !Z-1.0-1.noarch [11] (w1) Install.level1
   E-1.0-1.noarch [7] (w2)
   F-1.0-1.noarch [8]
   G-1.0-1.noarch [9]
   H-1.0-1.noarch [10]
   next rules: 0 0
 Rule #3:
   !H-1.0-1.noarch [10] (w1)
   !A-1.0-1.noarch [3] (w2) Install.level1
   next rules: 0 0
 Rule #4:
   !G-1.0-1.noarch [9] (w1)
   !B-1.0-1.noarch [4] (w2)
   next rules: 0 0
 Rule #5:
   !F-1.0-1.noarch [8] (w1)
   !C-1.0-1.noarch [5] (w2)
   next rules: 0 0
 Rule #6:
   !E-1.0-1.noarch [7] (w1)
   !D-1.0-1.noarch [6] (w2)
   next rules: 0 0

创建作业规则

 Rule #7:
   A-1.0-1.noarch [3] (w1) Install.level1
   next rules: 0 0
 Rule #8:
   Z-1.0-1.noarch [11] (w1) Install.level1
   next rules: 0 0

初始决策

初始决策是通过生成规则来做出的。这些决策（在队列 decisionq 和映射 decisionmap 中描述）在队列 decisionq_why 中没有条目。

 ----- Decisions -----
 SYSTEMSOLVABLE
 install A-1.0-1.noarch
 install Z-1.0-1.noarch
 ----- Decisions end -----

求解

传播决策

对于 decisionq 中的每个决策，将调用传播算法。将检查观察列表，如果此决策命中另一个规则，则将做出其他决策

----- propagate -----
popagate for decision 1 level 1
   system:system-.noarch [1] Install.level1
Watches: 
   solvable [-12] -- rule [0]
   solvable [-11] -- rule [1]
   solvable [-10] -- rule [3]
   solvable [-9] -- rule [4]
   solvable [-8] -- rule [5]
   solvable [-7] -- rule [6]
   solvable [-6] -- rule [6]
   solvable [-5] -- rule [5]
   solvable [-4] -- rule [4]
   solvable [-3] -- rule [3]
   solvable [-2] -- rule [0]
   solvable [-1] -- rule [0]
   solvable [0] -- rule [0]
   solvable [1] -- rule [0]
   solvable [2] -- rule [0]
   solvable [3] -- rule [1]
   solvable [4] -- rule [0]
   solvable [5] -- rule [0]
   solvable [6] -- rule [0]
   solvable [7] -- rule [2]
   solvable [8] -- rule [0]
   solvable [9] -- rule [0]
   solvable [10] -- rule [0]
   solvable [11] -- rule [0]
   solvable [12] -- rule [0]
popagate for decision 3 level 1
   A-1.0-1.noarch [3] Install.level1
Watches: 
   solvable [-12] -- rule [0]
   solvable [-11] -- rule [1]
   solvable [-10] -- rule [3]
   solvable [-9] -- rule [4]
   solvable [-8] -- rule [5]
   solvable [-7] -- rule [6]
   solvable [-6] -- rule [6]
   solvable [-5] -- rule [5]
   solvable [-4] -- rule [4]
   solvable [-3] -- rule [3]
   solvable [-2] -- rule [0]
   solvable [-1] -- rule [0]
   solvable [0] -- rule [0]
   solvable [1] -- rule [0]
   solvable [2] -- rule [0]
   solvable [3] -- rule [1]
   solvable [4] -- rule [0]
   solvable [5] -- rule [0]
   solvable [6] -- rule [0]
   solvable [7] -- rule [2]
   solvable [8] -- rule [0]
   solvable [9] -- rule [0]
   solvable [10] -- rule [0]
   solvable [11] -- rule [0]
   solvable [12] -- rule [0]
 watch triggered Rule #3:
   !H-1.0-1.noarch [10] (w1)
   !A-1.0-1.noarch [3] (w2) Install.level1
   next rules: 0 0
  unit Rule #3:
   !H-1.0-1.noarch [10] (w1)
   !A-1.0-1.noarch [3] (w2) Install.level1
   next rules: 0 0
   -> decided to conflict H-1.0-1.noarch
popagate for decision 11 level 1
   Z-1.0-1.noarch [11] Install.level1
Watches: 
   solvable [-12] -- rule [0]
   solvable [-11] -- rule [1]
   solvable [-10] -- rule [3]
   solvable [-9] -- rule [4]
   solvable [-8] -- rule [5]
   solvable [-7] -- rule [6]
   solvable [-6] -- rule [6]
   solvable [-5] -- rule [5]
   solvable [-4] -- rule [4]
   solvable [-3] -- rule [3]
   solvable [-2] -- rule [0]
   solvable [-1] -- rule [0]
   solvable [0] -- rule [0]
   solvable [1] -- rule [0]
   solvable [2] -- rule [0]
   solvable [3] -- rule [1]
   solvable [4] -- rule [0]
   solvable [5] -- rule [0]
   solvable [6] -- rule [0]
   solvable [7] -- rule [2]
   solvable [8] -- rule [0]
   solvable [9] -- rule [0]
   solvable [10] -- rule [0]
   solvable [11] -- rule [0]
   solvable [12] -- rule [0]
 watch triggered Rule #1:
   !Z-1.0-1.noarch [11] (w1) Install.level1
   A-1.0-1.noarch [3] (w2) Install.level1
   B-1.0-1.noarch [4]
   C-1.0-1.noarch [5]
   D-1.0-1.noarch [6]
   next rules: 2 0
 watch triggered Rule #2:
   !Z-1.0-1.noarch [11] (w1) Install.level1
   E-1.0-1.noarch [7] (w2)
   F-1.0-1.noarch [8]
   G-1.0-1.noarch [9]
   H-1.0-1.noarch [10] Conflict.level1
   next rules: 0 0
   -> move w1 to F-1.0-1.noarch
popagate for decision -10 level 1
   !H-1.0-1.noarch [10] Conflict.level1
Watches: 
   solvable [-12] -- rule [0]
   solvable [-11] -- rule [1]
   solvable [-10] -- rule [3]
   solvable [-9] -- rule [4]
   solvable [-8] -- rule [5]
   solvable [-7] -- rule [6]
   solvable [-6] -- rule [6]
   solvable [-5] -- rule [5]
   solvable [-4] -- rule [4]
   solvable [-3] -- rule [3]
   solvable [-2] -- rule [0]
   solvable [-1] -- rule [0]
   solvable [0] -- rule [0]
   solvable [1] -- rule [0]
   solvable [2] -- rule [0]
   solvable [3] -- rule [1]
   solvable [4] -- rule [0]
   solvable [5] -- rule [0]
   solvable [6] -- rule [0]
   solvable [7] -- rule [2]
   solvable [8] -- rule [2]
   solvable [9] -- rule [0]
   solvable [10] -- rule [0]
   solvable [11] -- rule [0]
   solvable [12] -- rule [0]
----- propagate end-----

处理未满足的规则

评估未满足的规则

需要描述。我仍然不明白。

为未满足的规则做出决策

 deciding unresolved rules
 unfulfilled Rule #2:
   !Z-1.0-1.noarch [11] Install.level1
   E-1.0-1.noarch [7] (w2)
   F-1.0-1.noarch [8] (w1)
   G-1.0-1.noarch [9]
   H-1.0-1.noarch [10] Conflict.level1
   next rules: 0 0
 prune_to_best_version 3
 - E-1.0-1.noarch
 - F-1.0-1.noarch
 - G-1.0-1.noarch
 installing E-1.0-1.noarch

传播新的决策

----- propagate -----
popagate for decision 7 level 2
   E-1.0-1.noarch [7] Install.level2
Watches: 
   solvable [-12] -- rule [0]
   solvable [-11] -- rule [1]
   solvable [-10] -- rule [3]
   solvable [-9] -- rule [4]
   solvable [-8] -- rule [5]
   solvable [-7] -- rule [6]
   solvable [-6] -- rule [6]
   solvable [-5] -- rule [5]
   solvable [-4] -- rule [4]
   solvable [-3] -- rule [3]
   solvable [-2] -- rule [0]
   solvable [-1] -- rule [0]
   solvable [0] -- rule [0]
   solvable [1] -- rule [0]
   solvable [2] -- rule [0]
   solvable [3] -- rule [1]
   solvable [4] -- rule [0]
   solvable [5] -- rule [0]
   solvable [6] -- rule [0]
   solvable [7] -- rule [2]
   solvable [8] -- rule [2]
   solvable [9] -- rule [0]
   solvable [10] -- rule [0]
   solvable [11] -- rule [0]
   solvable [12] -- rule [0]
 watch triggered Rule #6:
   !E-1.0-1.noarch [7] (w1) Install.level2
   !D-1.0-1.noarch [6] (w2)
   next rules: 0 0
  unit Rule #6:
   !E-1.0-1.noarch [7] (w1) Install.level2
   !D-1.0-1.noarch [6] (w2)
   next rules: 0 0
   -> decided to conflict D-1.0-1.noarch
popagate for decision -6 level 2
   !D-1.0-1.noarch [6] Conflict.level2
Watches: 
   solvable [-12] -- rule [0]
   solvable [-11] -- rule [1]
   solvable [-10] -- rule [3]
   solvable [-9] -- rule [4]
   solvable [-8] -- rule [5]
   solvable [-7] -- rule [6]
   solvable [-6] -- rule [6]
   solvable [-5] -- rule [5]
   solvable [-4] -- rule [4]
   solvable [-3] -- rule [3]
   solvable [-2] -- rule [0]
   solvable [-1] -- rule [0]
   solvable [0] -- rule [0]
   solvable [1] -- rule [0]
   solvable [2] -- rule [0]
   solvable [3] -- rule [1]
   solvable [4] -- rule [0]
   solvable [5] -- rule [0]
   solvable [6] -- rule [0]
   solvable [7] -- rule [2]
   solvable [8] -- rule [2]
   solvable [9] -- rule [0]
   solvable [10] -- rule [0]
   solvable [11] -- rule [0]
   solvable [12] -- rule [0]
----- propagate end-----

结果

 >!> Solution #1:
 >!> install A-1.0-1.noarch[test]
 >!> install Z-1.0-1.noarch[test]
 >!> install E-1.0-1.noarch[test]
 >!> installs=3, upgrades=0, uninstalls=0

问题情况

需要描述。

参见

SAT 求解器基础