openSUSE:Libzypp satsolver

Jump to: navigation, search
SAT solver library is the most powerful package dependency solver and repository storage system available for Linux.

Dependency solving

Solving dependencies is the core functionality for any software management application on Linux.

Dependencies are used to divide and share functionalities across multiple software elements.

Linux (and Unix) follows two basic concepts to implement Divide & Conquer - breaking a large problem into smaller, more manageable ones.

Every software package expresses the functionalities it provides to others and those it requires from others through dependencies.

The task of the dependency resolver is to check and fulfill all these relations when managing software.

Basic laws of resolving

The dependency solver tries to solve dependencies without user intervention based on two basic rules

  1. Fulfill the install/remove requests given at start
  2. Keep the (dependencies of the) installed system consistent

Since the solver treats every package alike, these rules have some major and sometimes unexpected implications. A broken dependency might result in removal of lots of packages - the resulting system is still consistent but probably highly unusable.


Features

Using a Satisfiability Solver to compute package dependencies. Its based on expressing package dependencies as a boolean satisfiability problem.

Background & Information

The sat solver implementation as it appears in openSUSE 11.0 is based on two major, but independent, blocks

  1. Using a dictionary approach to store and retrieve package and dependency information.
  2. Using satisfiability, a well known and researched topic, for computing package dependencies.

The basics of using a satisfiability solver to solve package dependencies are detailed in SAT solver basics and SAT solver internals for more.


Developer documentation

Version: HEAD Developer Documentation

Version: 11.3 Developer Documentation

Version: 11.2 Developer Documentation



See also

Tools and libraries using SAT solver.


External links