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 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...?)
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.