Bug#761948: SAT solver competitions

[Michael Schroeder <mls@suse.de>]

Libsolv is not a SAT solver, it's a package dependency solver. The SAT code
is just a very very small part of the code, and you really can't just plug
in a different SAT solver. The SAT algorithm does forced decisions
(i.e. when a rule is unit) and free decisions, in the later case solvers
like minisat pretty much randomly resolve a literal. But this is a
critical part of libsolv, as this is where the packages with the highest
version are chosen and the like.

Also, libsolv needs to record the decision chains so that it can support
solution introspection and also report meaningful suggestions if a problem
is unsolvable.

Finally, the code is optimized to minimize memory usage by making
advantage of the internal repository metadata format.