Title
Analyzing Context-Free Grammars Using an Incremental SAT Solver
Abstract
We consider bounded versions of undecidable problems about context-free languages which restrict the domain of words to some finite length: inclusion, intersection, universality, equivalence, and ambiguity. These are in (co)-NP and thus solvable by a reduction to the (un-)satisfiability problem for propositional logic. We present such encodings --- fully utilizing the power of incrementat SAT solvers --- prove correctness and validate this approach with benchmarks.
Year
DOI
Venue
2008
10.1007/978-3-540-70583-3_34
ICALP (2)
Keywords
Field
DocType
satisfiability problem,incrementat sat solvers,undecidable problem,analyzing context-free,propositional logic,incremental sat solver,context-free language,bounded version,finite length,sat solver,context free language,satisfiability,context free grammar
Discrete mathematics,Context-free grammar,Computer science,Correctness,Boolean satisfiability problem,Propositional calculus,Conjunctive normal form,Equivalence (measure theory),Propositional formula,Undecidable problem
Conference
Volume
ISSN
Citations 
5126
0302-9743
28
PageRank 
References 
Authors
1.81
10
3
Name
Order
Citations
PageRank
Roland Axelsson1493.44
Keijo Heljanko275147.90
Martin Lange3844.86