# Translation of context-free parsing into SAT

Is there a published algorithm for translating a context-free parsing problem into SAT? That is, an algorithm that translates a context-free grammar and an input string into a set clauses that is satisfiable iff the input string is well-formed according to the grammar.

• I do not know. There is a somewhat related translation of a CFG Ginto a Presburger formula for the Parikh image of L(G) in Theorem 4 o:f Kumar Neeraj Verma, Helmut Seidl, Thomas Schwentick: On the Complexity of Equational Horn Clauses. CADE 2005:337-352 (DOI:10.1007/11532231_25) – Thomas S Mar 6 '15 at 7:22

(I guess the important word in the original question is published''.) There is such an encoding of context-free parsing (more exactly of CYK-style parsing) in Roland Axelsson, Keijo Heljanko, and Martin Lange, Analyzing Context-Free Grammars Using an Incremental SAT Solver, ICALP 2008, Lecture Notes in Computer Science vol. 5126, pp. 410--422, doi:10.1007/978-3-540-70583-3_34. They use it in particular to detect ambiguity of words $w$ in context-free grammars for growing word lengths.