On the Existential Theories of Büchi Arithmetic and Linear p-adic Fields
2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)(2019)
摘要
We consider the complexity of the satisfiability problems for the existential fragment of Büchi arithmetic and for the existential fragment of linear arithmetic over p-adic fields. Our main results are that both problems are NP-complete. The NP upper bound for existential linear arithmetic over p-adic fields resolves an open question posed by Weispfenning [J. Symb. Comput., 5(1/2) (1988)] and holds despite the fact that satisfying assignments in both theories may have bit-size super-polynomial in the description of the formula. A key technical contribution is to show that the existence of a path between two states of a finite-state automaton whose language encodes the set of solutions of a given system of linear Diophantine equations can be witnessed in NP.
更多查看译文
关键词
bit-size super-polynomial,linear Diophantine equations,Büchi arithmetic,linear p-adic fields,satisfiability problems,NP-complete problem
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要