The Decision Problem for Undirected Graphs with Reachability and Acyclicity

We address the decision problem for a theory about undirected graphs with reachability and acyclicity predicates, denoted UGRA, encompassing graph and node variables, the basic Boolean set operators \(\cup \) , \(\cap \) , \(\setminus \) , singleton graphs, and predicates for acyclicity and reachability. By drawing from the well-established techniques of Computable Set Theory, we prove the decidability of the theory UGRA  by showing that it enjoys the following small model property: every satisfiable formula of UGRA  of size n admits a finite model of size \(\mathcal {O}(n^{8})\) . Such a property will also allow us to prove that the decision problem for UGRA  is NP-complete.