Hi, Thanks a lot for providing further information! > > 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. > I had suspected that there would be some domain-specific knowledge built into the solver logic. > 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. > That would be unsatisfiable cores in SAT solving terminology I'd say (and the existing solvers provide access to those). But adding meaningful remedy is obviously domain-specific, again (though a problem that the sat4j team necessarily looked at to make it work as eclipse's dependency resolver). > Finally, the code is optimized to minimize memory usage by making > advantage of the internal repository metadata format. > Maybe a good first step would be including some of the information that you kindly provided into the README file. As-is, it suggests that there's just a built-in SAT solver (especially the "Google for 'sat solver'" underlines this, IMHO). Thanks again, Michael
Attachment:
pgps0BVH8ZvPy.pgp
Description: PGP signature