Re: Re : Re: F18 Release Notes
On 09/18/2012 02:13 PM, Bruno Wolff III wrote:
On Tue, Sep 18, 2012 at 12:00:36 +0200,
Compte Yahoo <rforlot(a)yahoo.com> wrote:
>
> Why not. As I understand DNF is a fork of yum that uses new backend. I
> have a question, what is a SAT solver ? a satellite solver ?
http://en.wikipedia.org/wiki/Boolean_satisfiability_problem
Hello,
yes, SAT solver is a program that sees if a given boolean formula is
satisfiable (and with what assignments). libsolv (the DNF backend) does
just that: after it reduces the package dependency problem to a
conjunctive normal form it runs its SAT solver over it to see if it's
satisfiable (i.e. if any combination of all packages can be installed to
respect what the user selected for installation) and with what
assignments (what packages to specifically put into the transaction and
install/delete/...).
This is essentially different from what depsolvers in Yum, RPM and other
packaging software do: they usually build some sort of graph of packages
and their dependencies and then traverse it and add packages until all
deps and constrains are satisfied. The premise of using SAT solving
instead is that we get the minimal result, faster, with less memory
(besides SAT solving libsolv is being very smart about how to store the
package metadata).
HTH and sorry for no satellites here:)
Ales