Algorithmic meta-theorems state that problems that can be formalized in a fixed logic can be solved efficiently on classes of structures with certain properties. A prominent example is Courcelle's Theorem, which states that all problems expressible in monadic second-order logic can be solved efficiently on structures of small treewidth. Such theorems are usually proven by a generic algorithm for the model-checking problem of the given logic, which is often complex and rarely leads to highly efficient solutions. Alternatively, we can solve the model-checking problem by grounding the given logic to propositional logic, for which dedicated solvers are available. Such encodings will, however, usually not preserve the input's treewidth. This paper investigates whether all problems definable in monadic second-order logic can efficiently be encoded into SAT such that the input's treewidth bounds the treewidth of the resulting formula. We answer this in the affirmative and, hence, provide an alternative proof of Courcelle's Theorem. Our technique can naturally be extended: There are treewidth-aware reductions from the optimization version of Courcelle's Theorem to MaxSAT and from the counting version of the theorem to #SAT. By using encodings to SAT, we obtain, ignoring polynomial factors, the same running time for the model-checking problem as we would with dedicated algorithms. We complement our upper bounds with new lower bounds based on ETH; and we show that the block size of the input's formula and the treewidth of the input's structure are tightly linked. We also provide matching upper and lower bounds for a fragment of guarded MSO, only using SAT-based techniques.

翻译：算法元定理指出，能够在固定逻辑中形式化的问题可以在具有特定性质的结构类上高效求解。一个著名例子是Courcelle定理，该定理表明所有可用一元二阶逻辑表达的问题均可在树宽较小的结构上高效求解。此类定理通常通过给定逻辑模型检测问题的通用算法来证明，这些算法往往复杂且难以产生高效解法。另一种方法是将给定逻辑归约为命题逻辑（已有专用求解器支持此类归约），但这种编码通常无法保持输入的树宽。本文研究一元二阶逻辑可定义的所有问题能否高效编码为SAT，使得输入树宽约束生成公式的树宽。我们对此给出肯定回答，从而为Courcelle定理提供替代证明。该技术可自然扩展：存在从Courcelle定理优化版到MaxSAT的树宽感知归约，以及从计数版到#SAT的对应归约。通过使用SAT编码，我们在模型检测问题上获得与专用算法相同的运行时间（忽略多项式因子）。我们基于ETH给出新下界以补充上界分析，并证明输入公式的块大小与输入结构树宽存在紧密关联。此外，我们仅使用SAT技术为受保护MSO的片段提供了匹配的上下界。