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