hard.md

This is a Hard Problem

Generating strings from an attribute grammar is NP-Complete.

Outline

1. Reduction 3SAT -> AGSG [Shows AGSG at least NP-Hard]
2. Proof of Poly-Time Verifiable Certificate [AGSG in NP]

Since AGSG is NP-Hard and it is in NP it is NP-Complete.

Decision Problem

Is the language generated by this grammar the empty language?

Reduction, 3SAT -> AGSG [Attribute Grammar String Generation]

Construct a grammar for the 3SAT instance

eg.

(x1 || x2 || x3) && (x2 || ~x3 || x4) ... (x2 || x3 || x4)

becomes

SAT -> AndsM ;

AndM -> AndsM-1 AND ClauseM ;
...
And2 -> Ands1 AND Clause2 ;
And1 -> Clause1 ;

Clause1 -> '(' x1 OR x2 OR x3 ')' ;
Clause2 -> '(' x2 OR NOT x3 OR x4 ')' ;
...
ClauseM -> '(' x2 OR x3 OR x4 ')' ;

x1 -> TRUE
    | FALSE
    ;
x2 -> TRUE
    | FALSE
    ;
...
xN -> TRUE
    | FALSE
    ;

With attributes which synthesize the values for each clause and with a condition which asserts that the whole expression is true.

SAT -> AndsM
       with Condition {
         AndsM.value == True
       }
       ;

AndM -> AndsM-1 AND ClauseM
         with Action {
            AndsM.value = AndM-1.value && ClauseM.value
            AndsM.names = {
              ClauseM.a.name:ClauseM.a.value,
              ClauseM.b.name:ClauseM.b.value,
              ClauseM.c.name:ClauseM.c.value
            }
            AndsM.names = AndsM.names | AndsM-1.names
         }
         with Condition {
           (ClauseM.a.name != ClauseM.b.name ||
             ClauseM.a.value == ClauseM.b.value) &&
           (ClauseM.c.name != ClauseM.b.name ||
             ClauseM.c.value == ClauseM.b.value) &&
           (ClauseM.a.name != ClauseM.c.name ||
             ClauseM.a.value == ClauseM.c.value) &&
           (ClauseM.a.name not in AndsM-1.names ||
             ClauseM.a.value == AndsM-1.names[ClauseM.a.name]) &&
           (ClauseM.b.name not in AndsM-1.names ||
             ClauseM.b.value == AndsM-1.names[ClauseM.b.name]) &&
           (ClauseM.c.name not in AndsM-1.names ||
             ClauseM.c.value == AndsM-1.names[ClauseM.c.name])
         }
         ;
...
And2 -> Ands1 AND Clause2
         with Action {
            Ands2.value = Ands1.value && Clause2.value
            Ands2.names = {
              Clause2.a.name:Clause2.a.value,
              Clause2.b.name:Clause2.b.value,
              Clause2.c.name:Clause2.c.value
            }
            Ands2.names = Ands2.names | Ands1.names
         }
         with Condition {
           (Clause2.a.name != Clause2.b.name ||
             Clause2.a.value == Clause2.b.value) &&
           (Clause2.c.name != Clause2.b.name ||
             Clause2.c.value == Clause2.b.value) &&
           (Clause2.a.name != Clause2.c.name ||
             Clause2.a.value == Clause2.c.value) &&
           (Clause2.a.name not in Ands1.names ||
             Clause2.a.value == Ands1.names[Clause2.a.name]) &&
           (Clause2.b.name not in Ands1.names ||
             Clause2.b.value == Ands1.names[Clause2.b.name]) &&
           (Clause2.c.name not in Ands1.names ||
             Clause2.c.value == Ands1.names[Clause2.c.name])
         }
         ;
And1 -> Clause1
         with Action {
            Ands1.value = Clause1.value
            Ands1.names = {
              Clause1.a.name:Clause1.a.value,
              Clause1.b.name:Clause1.b.value,
              Clause1.c.name:Clause1.c.value
            }
         }
         with Condition {
           (Clause1.a.name != Clause1.b.name ||
             Clause1.a.value == Clause1.b.value) &&
           (Clause1.c.name != Clause1.b.name ||
             Clause1.c.value == Clause1.b.value) &&
           (Clause1.a.name != Clause1.c.name ||
             Clause1.a.value == Clause1.c.value)
         }
         ;

Clause1 -> '(' x1 OR x2 OR x3 ')'
           with Action {
             Clause1.value = x1.value || x2.value || x3.value
             Clause1.a.name = 'x1'
             Clause1.a.value = x1.value
             Clause1.b.name = 'x2'
             Clause1.b.value = x2.value
             Clause1.c.name = 'x3'
             Clause1.c.value = x3.value
           }
           ;
Clause2 -> '(' x2 OR NOT x3 OR x4 ')'
           with Action {
             Clause2.value = x2.value || !x3.value || x4.value
             Clause2.a.name = 'x2'
             Clause2.a.value = x2.value
             Clause2.b.name = 'x3'
             Clause2.b.value = x3.value
             Clause2.c.name = 'x4'
             Clause2.c.value = x4.value
           }
           ;
...
ClauseM -> '(' x2 OR x3 OR x4 ')'
           with Action {
             ClauseM.value = x2.value || x3.value || x4.value
             ClauseM.a.name = 'x2'
             ClauseM.a.value = x2.value
             ClauseM.b.name = 'x3'
             ClauseM.b.value = x3.value
             ClauseM.c.name = 'x4'
             ClauseM.c.value = x4.value
           }
           ;

x1 -> TRUE
      with Action {
        x1.value = True
      }
    | FALSE
      with Action {
        x1.value = False
      }
    ;
x2 -> TRUE
      with Action {
        x1.value = True
      }
    | False
      with Action {
        x1.value = False
      }
    ;
...
xN -> TRUE
      with Action {
        x1.value = True
      }
    | FALSE
      with Action {
        x1.value = False
      }
    ;

This translation from 3SAT to AGSG is clearly poly time. O(|C| + |V|) where C = the clauses in 3SAT and V = the variables.

Show a solution for 3SAT --> creates a parsable string for AGSG

In a solution for 3SAT all names (x1, x2, ... xN) always have exactly one value (True or False) assigned to them. The condition on each "AndX" production [And1, And2 ...] states that each name always has the same value. That is once xN has recieved a value (True or False) all other instances of xN must have the same value. Therefore, all conditions are the AndX clauses are satisfied by any solution to 3SAT by the definition of a 3SAT solution.

The actions on each variable production (x1, x2, ... xN) produce a value, eg. x1.value, either equal to True or False. The actions on each clause production (Clause1, Clause2, ... ClauseN) combine the values of the variables in that clause together. They combine them in the same way they are combined in the equivalent clause in 3SAT by construction.

Finally the chain of And productions (And1, And2, ... AndN) combine the values synthesized by the clauses (Clause1.value, Clause2.value, ... ClauseN.value). Into a final value AndN.value via:

And1.value = Clause1.value
And2.value = And1.value && Clause2.value
And3.value = And2.value && Clause3.value
...
AndN.value = AndN-1.value && ClauseN.value

which can be reduced to 1 expression with algebraic substitution as:

AndN.value = Clause1.value && Clause2.value && ... && ClauseN.value

Which synthesizes the same value which the 3SAT problem specifies. Once again by construction.

Therefore, if a variable assignment satisfies 3SAT then it must also synthesize a value of True on AndN.value resulting in a parsable expression.

Show a string generated by the grammar --> is a solution for 3SAT

In the above proof, we showed that the attributes on the grammar compute the same answer as algebraically evaulating the 3SAT expression. Since (once again by the above proof) there is a unique variable assignment in the generated string this string must evaluate to True. If it didn't it could not have been generated by the grammar. Therefore, the string generated corresponds to a unique variable assignment in 3SAT which causes the expression to evaluate to True.

AGSG is in NP

Certificate

A string of terminal symbols.

Show the Certificate can be Verified in Poly-Time

The Algorithm for Verification

• Transform the Context-Free grammar into Chomsky Normal Form. This ensures a polynomial tree height with each Non-Terminal symbol having at most 2 children.

• Using the Chomsky Normal Form Context-Free version of the grammar parse the string and transform it into a parse tree.

• Using a Post-Order tree traversal to apply the actions and check the conditions of each grammar rule

Proof Alg. in Poly-Time

Since the parse tree has a polynomial number of nodes there are only a polynomial number of steps. However, how bad can 1 of those steps be in the worst case? That is, how much time can it take to check a condition? Is it linear with respect to the input (which includes: the attribute grammar, and the certificate)?

To examine this we will start with the leaves of the parse tree. Each leaf is a Terminal Symbol. A constant number of attributes can be produced by a single terminal symbol. We denote this number as $C$. Therefore, there can be at most $C$ actions and $C^2 D$ terms in the condition -- where $D$ is the number of binary comparison operators in the language.

Most importantly, if the condition actually has $C^2 D$ terms every term has to be written down. So checking the truth value of the condition is linear with respect to the size of the attribute grammar. If loops or quantifiers such as $\exists$ and $\forall$ are allowed this no longer holds. However, since we do not allow quantification in the conditions checking a leaf condition (and indeed any condition) must be linear with respect to the size of the input.

At internal nodes the number of terms in a condition could be as high as $(2^{h-2}C)^2 D$ where $h$ is the height of the subtree rooted at the current node. Once again, while this is clearly an exponential number, it is not exponential with respect to the input as each term is part of the input.

Therefore,

checking all conditions are satisfied is polynomial time as long as quantifiers are disallowed from conditions.