On Tue, 30 May 2017 09:22:45 +0100 Ciaran McCreesh <[email protected]> wrote:
> On Tue, 30 May 2017 09:42:45 +0200 > Alexis Ballier <[email protected]> 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 ? > > Not hard as in you need a Ph.D. in algorithms to solve it but the > > kind of hardness almost every cryptographic algorithm used today, > > and in the foreseeable future, relies on. > > Hrm, you're a bit off, there. SAT solving in practice isn't usually > that bad unless either your inputs are huge or they're deliberately > crafted to be ultra-nasty. Being NP-complete just means that instances > that will hit exponential behaviour exist, not that those instances > will occur in the application area you care about. Yes, SAT is somewhat one of the easiest NP complete problems. Still, do we accept everyone having php installed to have its 'emerge -uDN world' consume 1 cpu-minute? 10 cpu-minutes? 60 cpu-minutes? What's the limit? How do we define 'ultra-nasty' constructs? How do we avoid them? Do we want to spec the solver's heuristic used so that developers can rely on it performing well on some constructs and poorly on some others? Do we want to spec some syntax so that PM developers can use an heuristic performing well on the instances provided? I really believe that's too many questions for something that can be solved efficiently in a simpler manner. Bests, Alexis.
