On the existential theories of Büchi arithmetic and linear p-adic fields
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-ad...
| Main Authors: | , , |
|---|---|
| Format: | Conference item |
| Published: |
IEEE
2019
|
| Summary: | 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. |
|---|