Home Wiki > openSUSE:Libzypp satsolver
Sign up | Login

openSUSE:Libzypp satsolver

tagline: From openSUSE

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


See also

Tools and libraries using SAT solver.


External links