Content deleted Content added
structuring, add more about computational complexity of evaluation, enumeration, and counting |
m →Computational complexity of evaluation: clarify |
||
Line 24:
By contrast, when we wish to check whether a Boolean MSO formula is satisfied by an input finite [[tree (data structure)|tree]], this problem can be solved in linear time in the tree, by translating the Boolean MSO formula to a [[tree automaton]]<ref>{{Cite journal|last=Thatcher|first=J. W.|last2=Wright|first2=J. B.|date=1968-03-01|title=Generalized finite automata theory with an application to a decision problem of second-order logic|url=https://doi.org/10.1007/BF01691346|journal=Mathematical systems theory|language=en|volume=2|issue=1|pages=57–81|doi=10.1007/BF01691346|issn=1433-0490}}</ref> and evaluating the automaton on the tree. In terms of the query, however, the complexity of this process is generally [[nonelementary problem|nonelementary]].<ref>{{Cite journal|last=Meyer|first=Albert R.|date=1975|editor-last=Parikh|editor-first=Rohit|title=Weak monadic second order theory of succesor is not elementary-recursive|url=https://link.springer.com/chapter/10.1007%2FBFb0064872|journal=Logic Colloquium|series=Lecture Notes in Mathematics|language=en|publisher=Springer Berlin Heidelberg|pages=132–154|doi=10.1007/bfb0064872.pdf|isbn=9783540374831}}</ref> Thanks to [[Courcelle's theorem]], we can also evaluate a Boolean MSO formula in linear time on an input graph if the [[treewidth]] of the graph is bounded by a constant.
For MSO formulas that have [[free variable]]s, when the input data is a tree or has bounded treewidth, there are efficient [[enumeration algorithm]]s to produce the set of all solutions<ref>{{Cite journal|last=Bagan|first=Guillaume|date=2006|editor-last=Ésik|editor-first=Zoltán|title=MSO Queries on Tree Decomposable Structures Are Computable with Linear Delay|url=https://link.springer.com/chapter/10.1007/11874683_11|journal=Computer Science Logic|series=Lecture Notes in Computer Science|language=en|publisher=Springer Berlin Heidelberg|pages=167–181|doi=10.1007/11874683_11|isbn=9783540454595}}</ref>, ensuring that the input data is preprocessed in linear time and that each solution is then produced in a delay linear in the size of each solution, i.e., constant-delay in the common case where all free variables of the query are first-order variables (i.e., they do not represent sets). There are also efficient algorithms for counting the number of solutions of the MSO formula in that case.<ref>{{Cite journal|last=Arnborg|first=Stefan|last2=Lagergren|first2=Jens|last3=Seese|first3=Detlef|date=1991-06-01|title=Easy problems for tree-decomposable graphs|url=http://www.sciencedirect.com/science/article/pii/019667749190006K|journal=Journal of Algorithms|volume=12|issue=2|pages=308–340|doi=10.1016/0196-6774(91)90006-K|issn=0196-6774}}</ref>
== Satisfiability ==
| |||