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