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 Axelsson | 1 | 49 | 3.44 |
Keijo Heljanko | 2 | 751 | 47.90 |
Martin Lange | 3 | 84 | 4.86 |