paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Linear equations for unordered data vectors in $[D]^k\to{}Z^d$

面向 [D]^k→Z^d 中无序数据向量的线性方程
LMCS vol.Volume 18, Issue 42022匹配度 2/10 · 论文属于逻辑与自动机方向,研究无序数据向量上的线性方程与扩展向量加法系统的可判定性,与形式化验证有间接理论关联;但未涉及用户核心关注的静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析,也没有工程落地、benchmark 或 LLM 交叉内容。引用 2 inbox
Piotr Hofman, Jakub Różycki
crossref: 2026-09-10

AI 速览

一句话:将线性方程推广到从无序数据集合的 k 元子集到整数向量的数据向量,并证明非负整数解在 NEXP、整数解在 P。

本文在近期关于无序数据向量和有序数据向量线性方程的一般化基础上,进一步把研究对象推广为从无序数据集的 k 元子集到整数向量的函数,即更一般的无序数据向量。此类广义线性方程并非人为构造,而是自然出现在对向量加法系统(Petri 网)的扩展分析中:其中每个 token 携带一个无序数据集合。论文主要考察这类线性方程的可满足性及其复杂度。结果表明,非负整数解的存在性可在非确定性指数时间(NEXP)内判定,而整数解的存在性则可在多项式时间(P)内判定。该工作给出了数据向量线性方程复杂度的新边界,并为分析带数据的 Petri 网/向量加法系统提供了理论工具。

问题
如何把线性方程的可满足性问题推广到从无序数据集的 k 元子集到整数向量的数据向量,并确定其判定复杂度?
方法
将数据向量定义为 [D] 的 k 元子集到 Z^d 的函数,建立相应的广义线性方程,并把它与每个 token 携带无序数据集合的向量加法系统(Petri 网)分析相联系。
评估
通过理论复杂度分析证明:非负整数可满足性属于 NEXP,而整数可满足性属于 P。
原文摘要(Abstract)

Following a recently considered generalisation of linear equations to unordered-data vectors and to ordered-data vectors, we perform a further generalisation to data vectors that are functions from k-element subsets of the unordered-data set to vectors of integer numbers. These generalised equations naturally appear in the analysis of vector addition systems (or Petri nets) extended so that each token carries a set of unordered data. We show that nonnegative-integer solvability of linear equations is in nondeterministic exponential time while integer solvability is in polynomial time.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot1638,
  title = {Linear equations for unordered data vectors in $[D]^k\to{}Z^d$},
  author = {Piotr Hofman and Jakub Różycki},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 18, Issue 4},
  year = {2022},
  doi = {10.46298/lmcs-18(4:11)2022}
}