Guepin, F;
Haase, C;
Worrell, J;
(2019)
On the Existential Theories of Büchi Arithmetic and Linear p-adic Fields.
In:
Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS).
IEEE: Vancouver, BC, Canada.
Preview |
Text
Haase_ghw-19 (002).pdf - Accepted Version Download (355kB) | Preview |
Abstract
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.
| Type: | Proceedings paper |
|---|---|
| Title: | On the Existential Theories of Büchi Arithmetic and Linear p-adic Fields |
| Event: | 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) |
| ISBN-13: | 9781728136080 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1109/LICS.2019.8785681 |
| Publisher version: | https://doi.org/10.1109/LICS.2019.8785681 |
| Language: | English |
| Additional information: | This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions. |
| Keywords: | Cost accounting, Automata, Upper bound, Encoding, Computational complexity, Digital arithmetic |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10089190 |
Archive Staff Only
 |
View Item |
