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. -- To UNSUBSCRIBE, email to debian-bugs-dist-requ...@lists.debian.org with a subject of "unsubscribe". Trouble? Contact listmas...@lists.debian.org
