Alexis Ballier <aball...@gentoo.org> wrote: > > I think we should really try to find a sub-exponential solution
Most examples mentioned earlier were actually 2SAT, i.e., they are only of the form foo? ( bar ) (possibly with negations) or can be easily reduced to that. E.g. ^^ ( foo bar ) foo? ( !bar graulty bazola ) can be rewritten as 2 or 3 2SAT-clauses as above, respectively. For 2SAT, there are linear time algorithms. If besides the above there occur not many clauses which are longer than 2 terms of the form ^^ ( foo !bar !graulty bazola ) then each such clause "just" multiplies the time by its size. (Yes, this is exponential, but I doubt that there will be many such clauses with more than 2 terms). The only problem which can really trigger a worst case (if the algorithm always reduces to solving a 2SAT problem) are longer || ( .... ) clauses. Either one should by definitoin limit the total number of USE-flags involved in those, or simply try only a limited combination of those (perhaps even only 1) and report a failure if this cannot be resolved (although an exponential time algorithm might be able to solve it).
