分层自动机中的标签割：Regular 约束的短解释
Label Cuts in Layered Automata: Short Explanations for the Regular Constraint
- Southern University of Science and Technology（南方科技大学）
- Guangdong Police College（广东警官学院）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
本文研究 Regular 约束的 LCG 解释，证明值删除解释等价于分层 DFA 的标签 s-t 割，确立最小权重解释的 NP 完全性，提出包含最小解释的多项式算法和精确动态规划，实验表明最小标签割显著缩短解释并高效运行。
AI中文摘要：
惰性子句生成求解器从传播解释中学习；因此，Regular 解释的形式决定了哪些子句到达学习引擎。标准分解引入自动机状态的变量，并从局部表约束中推导原因。BDD 和 MDD 传播器则选择单个图边。我们研究 Regular 的直接 LCG 解释语言：形式为 $X_i\ eq v$ 的不等文字。这里，一个文字移除具有相同位置/值标签的每个自动机转移，因此解释不是普通的边割。我们证明值删除的解释正是分层 DFA 展开中的标签 $s$--$t$ 割。这一刻画确立了最小权重解释的 NP 完全性，给出了包含最小解释的多项式算法，并导致对小自动机的精确 $O((U+n)4^{|Q|})$ 动态规划。一个 C++ 基准测试将标签割解释与 Table-LCG 和 MDD 边基线在 250 个生成实例上进行比较。平均而言，最小标签割将投影解释大小从 22.2 个文字减少到 5.5 个文字，并在几十微秒内运行。因此，最小标签割是实用的默认选择；精确算法为小自动机提供了预言机。
英文摘要：
Lazy clause generation solvers learn from propagation explanations; the form of a Regular explanation therefore determines which clauses reach the learning engine. Standard decompositions introduce variables for automaton states and derive reasons from local table constraints. BDD and MDD propagators instead select individual diagram edges. We study the direct LCG explanation language for Regular: disequality literals of the form $X_i\neq v$. Here, one literal removes every automaton transition with the same position/value label, so an explanation is not an ordinary edge cut. We prove that explanations for value deletions are exactly label $s$--$t$ cuts in the layered DFA unfolding. This characterization establishes NP-completeness for minimum-weight explanations, gives a polynomial algorithm for inclusion-minimal explanations, and leads to an exact $O((U+n)4^{|Q|})$ dynamic program for small automata. A C++ benchmark compares label-cut explanations with Table-LCG and MDD-edge baselines on 250 generated instances. On average, minimal label cuts reduce projected explanation size from 22.2 to 5.5 literals and run in tens of microseconds. Minimal label cuts are therefore the practical default; the exact algorithm provides an oracle for small automata.
