Ciaran McCreesh <ciaran.mccre...@googlemail.com> wrote: >> For 2SAT, there are linear time algorithms. > > "foo? ( bar )" does not encode as "( !foo \/ bar )"
It does (see below). More precisely, at first it encodes as an arrow foo -> bar in the implication graph. > Good luck figuring out how to encode grounding in SAT Easy game (in the 2SAT case): 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 whether we _enable_ or _disable_: We want a certain algorithm, specified by the order of the entries. If I understood the suggestion correctly, the algorithm would be: 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. Doing some pre-indexing, when parsing the string, it is easy to implement this checking in linear running time (in the size of the component). Hence, altogether linear running time is needed for the full algorithm (i.e. to process all components).
