Courcelle's Theorem

• bounded treewidth -> monadic second order logic (MSO) は線形時間で判定可
  • first order logic: 変数について quantifier がつけられる
    • ちょうど k （定数）個存在する，という quantifier も OK らしい．
  • monadic second order logic: 頂点集合 (≒boolean 関数) にも quantifier がつけられる
  • MSO2: 辺集合にも quantifier がつけられる
• feedback vertex set, SAT, ...