Exercise:

Judging exercises on CFGs
The coordinator of the «Theory of Computation» subject in our university wants to create a website that automatically evaluates exercises on context-free grammars (CFGs). The idea is that, for each exercise, the teacher simply prepares a reference solution CFG G1G_1, and then, any CFG G2G_2 submitted by a student is automatically compared against G1G_1 to determine whether they are equivalent (i.e., whether G1G_1 and G2G_2 generate the same language). Unfortunately, it is not possible to create such an evaluator, as equivalence of CFGs is an undecidable problem. Nevertheless, it is possible to implement a less ambitious automatic evaluator as follows: for each length \ell (up to a certain maximum), test whether there exists a word ww with length \ell that is generated by one of G1,G2G_1,G_2 but not by the other. Clearly, when such word ww exists, then ww is a counterexample to the equivalence of G1G_1 and G2G_2. When no such ww exists, either G1G_1 and G2G_2 are indeed equivalent, or we did not test with an \ell big enough to find a counterexample. There are many possible ways to implement an algorithm that, given G1,G2G_1,G_2 and \ell, looks for such counterexample ww; here we consider one possible technique.

Solve the following exercise by means of a reduction to SAT: The input of the exercise and the output with the solution (when the input is solvable) are as follows:
Authors: Carles Creus / Documentation:
To be able to submit you need to either log in, register, or become a guest.