Package Management/Sat Solver

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

• See FOSDEM 2008 presentation
• See Schroeder's FOSDEM 2008 video talk

General information.

• See the history of SAT solver.
• See the motivation, and the available FOSDEM2008 presentation.

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 here. See the internals page for more.

Get in touch with the ZYpp community.

Mailing Lists

Be sure to be subscribed to the zypp-devel mailing list when working on sat-solver

Documentation

Version: git head

C Developer Documentation

Version: git head

Ruby Developer Documentation

Version: 11.1

Developer Documentation (SOON)

Getting the source

Version: git head

libsatsolver HEAD

• For generic git instructions Git.
• For generic git.opensuse.org git instructions Git Hosting.

Anonymous clone

git clone git://git.opensuse.org/projects/zypp/sat-solver.git

Authorized clone

git clone git@git.opensuse.org:projects/zypp/sat-solver.git

Web repository browsing

• Available here.

Tools and libraries using SAT solver.

ZYpp – ZYpper – SUSE Studio