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.

  • 2
    $\begingroup$ 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) $\endgroup$
    – Thomas S
    Commented Mar 6, 2015 at 7:22

2 Answers 2


(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.


here is a similar/ more recent ref (2014) using the technique on probabilistic CFGs. (but they seem to skip over details of the SAT solver...?)

Grammatical Inference of some Probabilistic Context-Free Grammars from Positive Data using Minimum Satisfiability / Scicluna, Higuera

Recently, different theoretical learning results have been found for a variety of context-free grammar subclasses through the use of distributional learning (Clark, 2010b). However, these results are still not extended to probabilistic grammars. In this work, we give a practical algorithm, with some proven properties, that learns a subclass of probabilistic grammars from positive data. A minimum satisfiability solver is used to direct the search towards small grammars. Experiments on typical context-free languages and artificial natural language grammars give positive results.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.