Approximate Satisfiability and Equivalence
Eliana O. Fischer, Frédéric Magniez, Michel de Rougemont · 2006
Inspired by property testing, we relax the classical satisfiability UvDashF between a finite structure U of a class K and a formula F, to a notion of epsiv-satisfiability UvDashepsivF, and the classical equivalence F1equivF2between two formulas F1and F2, to epsiv-equivalence F1equivepsivF2for epsiv>0. We consider the class of strings and trees with the edit distance with moves, and show that these approximate notions can be efficiently decided. We use a statistical embedding of words (resp. trees) into lscr1, which generalizes the original Parikh mapping, obtained by sampling O(f(epsiv)) finite samples of the words (resp. trees). We give a tester for equality and membership in any regular language, in time independent of the size of the structure. Using our geometrical embedding, we can also test the equivalence between two regular properties on words, defined by monadic second order formulas. Our equivalence tester has polynomial time complexity in the size of the automaton (or regular expression), for a fixed epsiv, whereas the exact version of the equivalence problem is PSPACE-complete. Last, we extend the geometric embedding, and hence the tester algorithms, to infinite regular languages and to context-free languages. For context-free languages, the equivalence tester has an exponential time complexity, whereas the exact version is undecidable