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

[Martin Vaeth]

Martin Vaeth <martin@×××××.de> wrote:

Let me be more precise to avoid misunderstandings:

> For the "standard" 2SAT case, one first determines the strongly
> connected components in the implication graph (linear time).
> Then for each such component one either _enables_ or _disables_
> all vertices.
> The only difference to this "standard" 2SAT case is that we do
> not want a random choice here

This choice applies of course only to the _roots_ of the
reduced implication graph (which has strongly connected
components collapsed to vertices). In other words: Only for
those strongly connected components which have no predecessor
in the reduced implication graph, we can apply the subsequent
algorithm. (For the other components, one has to follow the
arrows in the reduced implication graph, of course.)

> Look for that implication arrow in the strongly connected component
> which occurs first in the specified ENFORCE_USE string; if
> the starting vertex of this arrow is enabled, then enable also
> the rest, otherwise disable it.

By "starting vertex" I meant here that vertex which is written
in front of ?. For instance, in a? ( b ) the "starting vertex"
is "a" while in !b? ( !a ) the "starting vertex" is "!b".
(Recall that every USE-flag "a" occurs as 2 vertices in the
implication graph: Once as "a" and once as its negation "!a".)

The 2-clause || ( a b ) has to be interpreted as !b? ( a ), of course.
For ^^ ( a b ) it does probably not matter whether it is interpreted as
a? ( !b ) !b? ( a )
or in the opposite order
!b? ( a ) a? ( !b )