Package Management/Sat Solver

From openSUSE

Categore:Code11

SAT-Solver

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

Background

See here for the motivation. There's also a presentation available.

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.

Theory

Google for 'sat solver' to get links to the theory behind it. This link gives a collection of bookmarks related to this topic.

Basics

The basics of using a satisfiability solver to solve package dependencies are detailed here.

Implementation

See the internals page for more.