openSUSE:Libzypp satsolver

Libzypp> Sat solver

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.

Make each program do one thing well. See Basics of the Unix Philosophy for details.
Use shared libraries to share implementations and save disk and memory space

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

Fulfill the install/remove requests given at start
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

Using a dictionary approach to store and retrieve package and dependency information.
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.