3-SAT Re: Blowout

[Rick Jelliffe <ricko@allette.com.au>]

Just to tidy up loose ends.

From: Henry S. Thompson <ht@cogsci.ed.ac.uk>

>I'm curious as to the collective wisdom wrt the usual (in
>computational linguistics) way of checking the worst-case complexity
>of grammar formalisms:  can you encode 3-SAT in TREX, RELAX,
>Schematron?

>For example:
>
>  (a v b v ~c) ^  (~b v d v ~e)  ^ (~a v c v e) ^ (~c v ~d v ~e)
>
>a=1
>b=0
>c=1
>d=0
>e=1
>
>satisfies this.

With implicit negation, the Schematron schema fragment is something like:

<assert test=
  " (a or b or not(c)) and
     (not(b) or d or not(e)) and
     (not(a) or c or e) and
     (not(c) or not(d) or not(e))" />

Note that, because we don't have to consume input sequentially against an
FSM, there seems no possiblity for explosions or expontiality here.

Cheers
Rick Jelliffe