1 |
On Tue, 30 May 2017 09:56:07 +0100 |
2 |
Ciaran McCreesh <ciaran.mccreesh@××××××××××.com> wrote: |
3 |
|
4 |
> On Tue, 30 May 2017 10:46:54 +0200 |
5 |
> Alexis Ballier <aballier@g.o> wrote: |
6 |
> > On Tue, 30 May 2017 09:22:45 +0100 |
7 |
> > Ciaran McCreesh <ciaran.mccreesh@××××××××××.com> wrote: |
8 |
> > > On Tue, 30 May 2017 09:42:45 +0200 |
9 |
> > > Alexis Ballier <aballier@g.o> wrote: |
10 |
> > > > Oh crap, this requires to solve SAT. |
11 |
> > > |
12 |
> > > The main problem would not be solving SAT, in this case. The |
13 |
> > > problem is providing the right answer when not enough information |
14 |
> > > is given. Spitting out a resolution which satisfies every |
15 |
> > > dependency isn't typically that difficult. Spitting out a |
16 |
> > > resolution which doesn't just turn off all your use flags and |
17 |
> > > uninstall most of your programs is the hard part. |
18 |
> > |
19 |
> > I don't really understand here: Assuming the formula is reduced |
20 |
> > where user-set useflags and profile-masked/forced ones are already |
21 |
> > assigned their true/false values, this leaves a formula with |
22 |
> > variables where changing any of those won't turn off (or on) |
23 |
> > anything you didn't want. If you can solve SAT on this reduced |
24 |
> > instance then you're safe, aren't you ? |
25 |
> |
26 |
> First problem: encoding "don't change this from its current setting |
27 |
> unless you have a reason to do so" is an utter pain in SAT. There are |
28 |
> other models like ASP that can just about get around this, but |
29 |
> expressing it properly is best done by just writing your own solver. |
30 |
> Remember that you have to allow the solver to toggle some flags, so |
31 |
> you can't just lock everything, but at the same time, you don't want |
32 |
> the solver to randomly toggle a flag that isn't specified by the user |
33 |
> or the profile, unless it absolutely has a good reason to do so. |
34 |
> |
35 |
> Second problem: a solver will spit out an arbitrary solution. If the |
36 |
> user then runs it again, there's no guarantee that it will spit out |
37 |
> the same arbitrary solution. That can be addressed by the right |
38 |
> choice of restart policies and tiebreaking etc if you're prepared to |
39 |
> muck around with the solver enough. But even if you do, suppose the |
40 |
> user thinks "yes, that's almost fine, but let me change one other |
41 |
> thing" (or if the install fails half-way through and the user tries |
42 |
> to carry on after fixing it). The solver will then spit out a totally |
43 |
> different arbitrary solution that looks nothing like the first one. |
44 |
|
45 |
|
46 |
The way I see it, this boils down to spec'ing something that guarantees |
47 |
there's a unique solution given an input. The solution does not have to |
48 |
be good or bad (we don't have a good metric on that anyway), it just |
49 |
has to be deterministic so that developers can arrange their |
50 |
REQUIRED_USE constraints to have PM chose the proper solution. |
51 |
|
52 |
|
53 |
Note: To me, the problems you describe are really the root of SAT |
54 |
solving problems (or any NP problem FWIW): An algorithm has to make |
55 |
choices that might have consequences arbitrary far and it might realize |
56 |
after running for a while that its initial assumption was invalid. |