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.
1
-
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 SMar 6, 2015 at 7:22
Add a comment
|
2 Answers
$\begingroup$
$\endgroup$
(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.
$\begingroup$
$\endgroup$
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.
