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. -- Ciaran McCreesh
