Structure-Guided Automated Reasoning

TL;DR

The paper presents a unified, structure-aware pipeline to ground model-checking for monadic second-order logic into SAT while preserving input treewidth, providing a SAT-based alternative to Courcelle's Theorem. It derives new, tight upper bounds for treewidth-preserving encodings (e.g., $\mathrm{tower}^*(\mathrm{qa}(\varphi)+1, k+3.92)$ for mc(mso) and $\mathrm{tower}^*(2, k+3.59)$ for pmc) by treewidth-aware quantifier elimination, and extends the approach to Fagin-definability with optimization and counting (maxSAT and #SAT). A full SAT version of Courcelle's Theorem is achieved through a modular encoding consisting of auxiliary encodings, quantifier indicators, and atom evaluation, yielding encodings of size $\mathrm{tower}^*(\mathrm{qa}(\varphi)+1,(k+9)|\varphi|+3.92)$ and treewidth $\mathrm{tower}(\mathrm{qa}(\varphi),(k+9)|\varphi|+3.92)$. ETH-based lower bounds tightly relate the encoding size to input formula block size and treewidth, and a compression scheme shows the trade-off between treewidth and quantifier blocks. Collectively, the results demonstrate that SAT-groundings can match the asymptotic running times of dedicated algorithms up to polynomial factors while clarifying fundamental limits on encoding size. This advances structure-guided automated reasoning by providing explicit, treewidth-aware translations from MSO model-checking, optimization, and counting to SAT, #SAT, and maxSAT.

Abstract

Algorithmic meta-theorems state that problems definable in a fixed logic can be solved efficiently on structures with certain properties. An 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 algorithms for the model-checking problem of the 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 \Lang{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. Another immediate consequence is a treewidth-preserving reduction from the model-checking problem of monadic second-order logic to integer linear programming (ILP). 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.

Figures (1)

• Figure 1: The reduction $\mathcal{R}_{\text{\normalfontmso}\rightarrow \text{\normalfontqsat}}(\varphi, \mathcal{S}, \mathcal{T})$ that takes as input an mso formula in prenex normal form $\varphi=Q_1 S_1\dots Q_{q-1} S_{q-1} Q_{q} s_q \dots Q_{\ell} s_\ell\mathop{\mathrm{\centerdot}}\nolimits \psi$ and a structure $\mathcal{S}$ with a TD $\mathcal{T}{=}(T,\mathop{\mathrm{\chi}}\nolimits)$ of $\mathcal{S}$ of width $k$. It obtains a QBF $\varphi'=Q_1 S_1'\dots Q_{\ell} S_\ell' \exists E' \mathop{\mathrm{\centerdot}}\nolimits \psi'$, where $\psi'$ is the conjunction of Equations (\ref{['redt:card']})--(\ref{['red:form']}), $S'_i=\{{(S_i)}_u \mid u\in U(\mathcal{S})\}$ and $E'=\mathop{\mathrm{\mathrm{vars}}}\nolimits(\psi')\setminus(\bigcup_{i=1}^{\ell} S'_i)$. Formula $\psi'$ can be easily converted into cnf of width linear in $k$ (for constant-size mso formulas $\varphi$).

Theorems & Definitions (8)

• Theorem 1: QBF Theorem
• Theorem 2: PMC Theorem
• Theorem 3: A SAT Version of Courcelle's Theorem
• Corollary 4
• Theorem 5: ETH Lower Bound
• Theorem 6: Trade-off Theorem
• Example 7
• Lemma 8