Martin Vaeth <mar...@mvath.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 )
