| 1 |
On Thu, 06 Nov 2014 14:25:46 +0100 |
| 2 |
Jauhien Piatlicki <jauhien@g.o> wrote: |
| 3 |
> Mathematics you said? That's nice. You can, for example, redesign our |
| 4 |
> portage's dependency solving algorithm, as it is quite slow at the |
| 5 |
> moment. ) I do not know what it does have inside right now, but using |
| 6 |
> SAT solver can be a good idea (there is a successful example already: |
| 7 |
> https://en.opensuse.org/openSUSE:Libzypp_satsolver) |
| 8 |
|
| 9 |
A SAT encoding for dependency resolution is a *terrible* idea, for all |
| 10 |
kinds of reasons (some of which are Gentoo-specific, and some of which |
| 11 |
are not). |
| 12 |
|
| 13 |
* The model would be full of implication constraints, which perform |
| 14 |
terribly under unit propagation. |
| 15 |
|
| 16 |
* You can't get decent human-readable explanations of failure out of SAT |
| 17 |
solvers. |
| 18 |
|
| 19 |
* You're not just trying to find a correct resolution. You're trying to |
| 20 |
find an optimal resolution, with respect to some very difficult |
| 21 |
criteria. For example, you don't want to install any extra unrelated |
| 22 |
packages. This is very hard to express in SAT if you're going for a |
| 23 |
model which preserves consistency. |
| 24 |
|
| 25 |
* Coming up with a legal ordering in SAT is a pain. It's worse if you're |
| 26 |
trying to fully solve circular dependencies: if you do, dependency |
| 27 |
resolution becomes harder than NP, so you'd at least need a QSAT |
| 28 |
solver, not SAT. |
| 29 |
|
| 30 |
* Coming up with a legal resolution isn't always the right thing to do. |
| 31 |
Often a legal resolution can be obtained by uninstalling a whole load |
| 32 |
of stuff or switching loads of USE flags off. But it's better to give a |
| 33 |
good error to the user than to come up with a legal but stupid |
| 34 |
resolution. In other words, you *don't* want a complete algorithm, you |
| 35 |
want a domain-aware incomplete algorithm. |
| 36 |
|
| 37 |
If you're going to go the toolkit route, you should be using a CP |
| 38 |
solver, not a SAT solver. But even then you'd be better off making some |
| 39 |
changes and not using plain old MAC, so you're back to writing the |
| 40 |
algorithms yourself. |
| 41 |
|
| 42 |
What you need is for someone who understands CP and SAT to write a |
| 43 |
resolver using algorithms inspired by how CP and SAT solvers work, but |
| 44 |
not just blindly copying them. Doing this well is at least a full year |
| 45 |
Masters level project... |
| 46 |
|
| 47 |
-- |
| 48 |
Ciaran McCreesh |
Archives