Re: [gentoo-dev] [RFC] Forced/automatic USE flag constraints (codename: ENFORCED_USE)

[Alexis Ballier <aballier@gentoo.org>]

On Tue, 30 May 2017 09:56:07 +0100
Ciaran McCreesh <ciaran.mccreesh@googlemail.com> wrote:

> On Tue, 30 May 2017 10:46:54 +0200
> Alexis Ballier <aballier@gentoo.org> wrote:
> > On Tue, 30 May 2017 09:22:45 +0100
> > Ciaran McCreesh <ciaran.mccreesh@googlemail.com> wrote:  
> > > On Tue, 30 May 2017 09:42:45 +0200
> > > Alexis Ballier <aballier@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.