On Thu, 06 Nov 2014 14:25:46 +0100 Jauhien Piatlicki <[email protected]> wrote: > Mathematics you said? That's nice. You can, for example, redesign our > portage's dependency solving algorithm, as it is quite slow at the > moment. ) I do not know what it does have inside right now, but using > SAT solver can be a good idea (there is a successful example already: > https://en.opensuse.org/openSUSE:Libzypp_satsolver)
A SAT encoding for dependency resolution is a *terrible* idea, for all kinds of reasons (some of which are Gentoo-specific, and some of which are not). * The model would be full of implication constraints, which perform terribly under unit propagation. * You can't get decent human-readable explanations of failure out of SAT solvers. * You're not just trying to find a correct resolution. You're trying to find an optimal resolution, with respect to some very difficult criteria. For example, you don't want to install any extra unrelated packages. This is very hard to express in SAT if you're going for a model which preserves consistency. * Coming up with a legal ordering in SAT is a pain. It's worse if you're trying to fully solve circular dependencies: if you do, dependency resolution becomes harder than NP, so you'd at least need a QSAT solver, not SAT. * Coming up with a legal resolution isn't always the right thing to do. Often a legal resolution can be obtained by uninstalling a whole load of stuff or switching loads of USE flags off. But it's better to give a good error to the user than to come up with a legal but stupid resolution. In other words, you *don't* want a complete algorithm, you want a domain-aware incomplete algorithm. If you're going to go the toolkit route, you should be using a CP solver, not a SAT solver. But even then you'd be better off making some changes and not using plain old MAC, so you're back to writing the algorithms yourself. What you need is for someone who understands CP and SAT to write a resolver using algorithms inspired by how CP and SAT solvers work, but not just blindly copying them. Doing this well is at least a full year Masters level project... -- Ciaran McCreesh
signature.asc
Description: PGP signature
