Logical Approaches to Non-deterministic Polynomial Time over Semirings
Timon Barlag, Nicolas Fröhlich, Teemu Hankala, Miika Hannula, Minna Hirvonen, Vivian Holzapfel, Juha Kontinen, Arne Meier, Laura Strieker
TL;DR
This work extends logical characterizations of nondeterministic computation to semiring settings by developing semiring semantics for propositional, first-order, and existential second-order logics, culminating in ESO$_K^{=}$ as a bridge to NP over semirings ($\mathsf{NP}_{K}$). It identifies canonical complete problems for the Boolean part of $\mathsf{NP}_{K}$ via SAT$_{K}^{=}$ and the true existential theory of the semiring, and establishes analogue theorems to Fagin and Cook in this framework. The results draw connections between semiring-based provability, semiring-provenance models, and BSS machines over semirings, including a definability result for degree-4 polynomial feasibility over $\mathbb{R}_{\ge 0}$ within ESO$_{\mathbb{R}_{\ge 0}}^{=}$. Overall, the paper provides a unified logical and computational treatment of NP-like classes over diverse semirings, enriching metafinite and algebraic approaches to complexity. These insights potentially impact geometric, algebraic, and database provenance problems by offering a robust logical toolkit for semiring-annotated computation.
Abstract
We provide a logical characterization of non-deterministic polynomial time defined by BSS machines over semirings via existential second-order logic interpreted in the semiring semantics developed by Grädel and Tannen. Furthermore, we show that, similarly to the classical setting, the satisfiability problem of propositional logic in the semiring semantics is the canonical complete problem for this version of NP. Eventually, we prove that the true existential first-order theory of the semiring is a complete problem for the so-called Boolean part of this version of NP.