openSUSE:Libzypp satsolver basics

Libzypp> Sat solver

Basics - Internals - Development

This article presents the basics concept behind the SAT solver used in ZYpp.

The following is based on a presentation given by Michael Schröder at FOSDEM 2008.

The SAT problem

• SAT: Boolean satisfiability problem

find a True/False assignment to all variables of a boolean expression (AND/OR/NOT) so that it is True. NP complete

• Normalization:

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

The (...) terms are called Rules consisting of literals a, b, c can also be negated: -a

Example:

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

Solution: a = FALSE, b = TRUE, c = FALSE

Advantages of SAT

• Well researched problem
  • many example solvers available (chaff, minisat...)
• Very fast
  • package solving complexity is very low compared to other areas where SAT solvers are used
• No complex algorithms
  • solving just needs a couple of hundreds lines of code
• Understandable suggestions
  • solver calculates proof why a problem is unsolvable

From dependencies to rules

Requires: package dependencies

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

“either A is not installed or one of B1, B2, B3 is installed”

Conflicts: package dependencies

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

“either A is not installed or B1 is not installed”

Obsoletes: package dependencies

treated as conflicts

More on making rules

Unary rules:

(-A)	Package A cannot be installed
	nothing provides a requirement, wrong arch, ...
	erase request (job rule)
(A)	Package A must be installed
	install request (job rule)

TRUE/FALSE values:

TRUE:	package will installed
FALSE:	package will not be installed/will be uninstalled

Solver algorithm

Unit propagation

A Rule is called unit, if all literals but one are FALSE
If a Rule is unit, the remaining literal can be set to TRUE Example:

(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

Algorithm

1. free choice: find some undecided variable, assign TRUE or FALSE
2. propagate all unit rules
3. repeat until all variables are decided

Unit propagation & dependencies

Requires rule (-A | B1 | B2 | B3)

• A, B1, B2 is FALSE → B3 must be TRUE
  • “If A is installed and all but one of the providers of a requires dependency cannot be installed, the remaining one must be installed”
  • → adds packages to the install set
• B1, B2, B3 is FALSE → A must be FALSE
  • “If none of the provides of a required dependency can be installed, the requiring package cannot be installed”
  • → adds packages to the conflicts/erase set

Conflicts rule (-A | -B1)

• A is TRUE → B1 must be FALSE and vice versa

Contradictions

Unit propagation can lead to a contradiction
This means that a literal must be both TRUE and FALSE
Example

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

if solver sets a to TRUE → b, c is TRUE, c is FALSE!

• learn new rule from rules involved in contradiction
  • → learned rule is (-a)
  • undo last free assignment and continue solving
  • if nothing to undo, problem was unsolvable

First implemented in 1996 in the GRASP solver.

Dealing with free choices

Here is where you influence the quality of the solution:

• try to keep packages installed
• minimize number of packages to install

Algorithm

1. if a package was installed before and is not in the conflicts set, install it
2. if a rule is not TRUE, but all of the negative literals are FALSE, choose best of the undecided positive literals and install the corresponding package
   (-A | B1 | B2) A TRUE → choose B1 or B2
3. do not install any other package (i.e. set all undecided variables to FALSE)

System policies

A policy rule defines what to do with installed packages

• must not be deinstalled or downgraded
• must not change architecture
• must not change vendor

Rule format:

(A | A2 | A3 | A4)

A2/A3/A4 are the allowed update candidates (same name and newer version or package with matching Obsoletes: dependency)

Reporting conflicts

If a problem turns out to be unsolvable, the solver algorithm will return a set of rules that led to the conflict.

As a system with no rpms installed is conflict free, the returned set of rules must contain at least one job rule or policy rule.

A possible solution is to remove one of those rules, i.e. remove a job (do not try to install package 'foo') or a policy rule (allow deinstallation of package 'bar')

Advantage: users understand those rules!

Conclusion

Using SAT solver algorithms solve many of the problems the old solver had

• speed: magnitudes faster
• reliable results
• extendibility: implementation of complex dependencies is easy
• sensible error reports

We're also working on a new repository format that can be processed much faster new dictionary based SOLV format.

---

See also

• SAT solver internals