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...
| Автори: | , , |
|---|---|
| Формат: | Conference item |
| Опубліковано: |
IEEE
2019
|
| _version_ | 1826289810922274816 |
|---|---|
| author | Guépin, F Haase, C Worrell, J |
| author_facet | Guépin, F Haase, C Worrell, J |
| author_sort | Guépin, F |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-07T02:34:35Z |
| format | Conference item |
| id | oxford-uuid:a85cdf1b-189c-43b2-8800-105f3b36cfb5 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T02:34:35Z |
| publishDate | 2019 |
| publisher | IEEE |
| record_format | dspace |
| spelling | oxford-uuid:a85cdf1b-189c-43b2-8800-105f3b36cfb52022-03-27T03:01:02ZOn the existential theories of Büchi arithmetic and linear p-adic fieldsConference itemhttp://purl.org/coar/resource_type/c_5794uuid:a85cdf1b-189c-43b2-8800-105f3b36cfb5Symplectic Elements at OxfordIEEE2019Guépin, FHaase, CWorrell, JWe 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. |
| spellingShingle | Guépin, F Haase, C Worrell, J On the existential theories of Büchi arithmetic and linear p-adic fields |
| title | On the existential theories of Büchi arithmetic and linear p-adic fields |
| title_full | On the existential theories of Büchi arithmetic and linear p-adic fields |
| title_fullStr | On the existential theories of Büchi arithmetic and linear p-adic fields |
| title_full_unstemmed | On the existential theories of Büchi arithmetic and linear p-adic fields |
| title_short | On the existential theories of Büchi arithmetic and linear p-adic fields |
| title_sort | on the existential theories of buchi arithmetic and linear p adic fields |
| work_keys_str_mv | AT guepinf ontheexistentialtheoriesofbuchiarithmeticandlinearpadicfields AT haasec ontheexistentialtheoriesofbuchiarithmeticandlinearpadicfields AT worrellj ontheexistentialtheoriesofbuchiarithmeticandlinearpadicfields |