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