# openSUSE:Libzypp satsolver internals

## Internals

### Pool and sources

### Rules

#### Definition of a rule

There are some kind of rules:

- Direct Assertion: e.G. (A) = install A; (-A) = remove A

- Binary Rule: e.G. (!A|B) = A requires B

- Rules with more than 2 possibilities: (!A|B1|B2 ) = A requires B1 OR B2

A rule contains a single literal (*called p*) and a pointer on an array of literals (*called d*).
Here some examples:

p = direct literal; always < 0 for installed rpm rules

d, if < 0 direct literal, if > 0 offset into whatprovides, if == 0 rule is assertion (look at p only)

- Install: p > 0, d = 0 (A) user requested install
- Remove: p < 0, d = 0 (-A) user requested remove
- Requires: p < 0, d > 0 (-A|B1|B2|...) d: <list of providers for requirement of p>
- Updates: p > 0, d > 0 (A|B1|B2|...) d: <list of updates for solvable p>
- Conflicts: p < 0, d < 0 (-A|-B) either p (conflict issuer) or d (conflict provider) (binary rule)
- No-op ?: p = 0, d = 0 (null) (used as policy rule placeholder)

#### Rule array

Rules are stored in an **array**. Additional the rules are grouped in the array:

rpm rules of involved packages |

job rules |

installed solvable rules (installed rule) |

weak rules (i.e. rules that get autodisabled if unsolvable) |

learnt rules |

Most groups have defined offsets variables:

solv->learntrules

solv->weakrules

solv->systemrules

solv->jobrules

The length of this array is defined by:

solve->nrules

### Jobs

Jobs are stored in a job queue. Each job has two elements:

**how**:- 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

**what**:- id of solvables
**OR** - id of provided string
**OR** - id of dependency

- id of solvables

### Watch array

The watch array will be generated before the solver starts solving and will be updated while a solver run. Watches get triggered when the corresponding literal goes False. As there are positive and negative literals we need nsolvables*2 entries. Each entry is a linked list through all of the involved rules.

The information how the watch array will be built is taken from each rule. A rule has two defined watchpoints (w1,w2) which depends on the kind of rule:

- Direct assertion (no watch needed)( if d <0 ) --> d = 0, w1 = p, w2 = 0
- Binary rule: p = first literal, d = 0, w2 = second literal, w1 = p
- Every other : w1 = p, w2 = whatprovidesdata[d];
- Disabled rule: w1 = 0

( *p* and *d* are explained in the rule definition chapter)

The watch array has nsolvables*2 entries and is addressed from the middle

- middle-solvable : decision to conflict, offset point to linked-list of rules
- middle+solvable : decision to install: offset point to linked-list of rules

So the index is the solvable ID (negativ or positiv) and the value will be the concerning watchpoint of a rule. For each rule these watchpoint will be regarded in the watch array:

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; }

An already defined watchpoint will be stored in n1 or n2 of the concerning rule **before** it will be overwritten by the new watchpoint.

### Decisions

Decisions are stored in 3 different queues/maps.

#### decisionq

Is a queue of solvables IDs and reflects the state which solvable will be installed(positiv ID) or will be deleted(negativ ID).

The length of this queue will be stored in decisionq.count .

#### decisionmap

The index is the ID of the concerning solvable. The value reflects the decision level of installation(positiv) or conflict(negativ).

#### decisionq_why

Is a queue of rule IDs that corresponds to the decisionq. This queue saves the reason why the solver made the decision. A reason is either a rule index if the decision was made because of a rule going unit, or "0".

The value can be "0" if:

- The concerning solvable is the SYSTEMRESOLVABLE, which is always installed.
- The decision is a rpm rule assertion only. We do not create rules for those.
- The decision was done by arbitrary choice.

The length of this queue will be stored in decisionq_why.count .

## How does the SAT solver work

The best way to get an overview about the solver workings would be to explain it with simple examples.

### Best case (without problems)

Environment:

Package | 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 |

Task:

Package | action |
---|---|

A | install |

B | install |

#### Building rules

Create rpm rules for packages involved with a job:

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

Creating job rules:

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

#### Initial decision

Initial decisions will be taken by generating the rules. These decisions (descibed in the queue *decisionq* and the map *decisionmap*) have 0 entries in the queue *decisionq_why*.

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

#### Solving

##### Propagate a decision

For each decision in the *decisionq* the propagate algorithm will be called.
There will be checked the watch list if this decision hits another rule for
this rule additional decisions will be made:

----- 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-----

##### Handle unfulfilled rules

###### Evaluate unfulfilled rules

Has to be described. I have still not understand.

###### Make decisions for unfulfilled rules

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 new decisions

----- 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-----

#### Results

>!> 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

### Problem case

Has to be described.