状态空间模型中可满足性问题的计算复杂度

基于摘要分析。本文研究 State Space Models（SSM）的可满足性问题 ssmSAT：是否存在一个输入序列，能使模型到达接受配置。核心贡献是分析一般情形及两类受限情形的可判定性与计算复杂度，为 SSM-based language models 的形式化推理与验证提供理论边界。 作者报告，一般情形下 ssmSAT 不可判定。对于上下文长度有界的 SSM，当输入长度以一元编码给出时，ssmSAT 为 NP-complete；当输入长度以二进制编码给出时，问题属于 NEXPTIME，且为 PSPACE-hard。后一个结论给出了上界和困难性下界，不能据此写成 NEXPTIME-complete。 第二类限制是采用定宽算术的量化 SSM。作者报告，随位宽编码方式不同，ssmSAT 分别为 PSPACE-complete 或属于 EXPSPACE；摘要未明确列出编码方式与这两个结论的具体对应关系，需核对全文。这些结果适用于 diagonal gated SSM，作者还为 time-invariant SSM 建立了复杂度界，但摘要未提供后一类模型的具体界。 技术上的阅读重点是：限制上下文长度或算术精度，可以使原本不可判定的问题变为可判定，但可判定并不意味着在实际规模上容易求解。输入长度和位宽的编码方式也是结论成立的关键背景，不能脱离编码协议比较复杂度。接受配置、输入域、量化运算的形式定义，以及证明所用的归约和算法构造尚未验证；摘要也未提供实际验证工具或运行性能证据。 本文主要对象是 SSM 的理论计算能力与形式化验证，而非 EEG 解码或 BCI 实验。材料未建立这些复杂度结论与神经信号任务之间的具体对应关系，因此不据此推断 BCI 有效性或提出迁移实验；已有 EEG 相关工作尚未检索确认。