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