Algorithmic Problems for Computation Trees
Mikhail Moshkov
TL;DR
The paper studies three algorithmic problems for computation trees over arbitrary structures: optimization, solvability, and satisfiability. It formalizes computation trees, problem schemes, and their relations, establishing decidability links between solvability and satisfiability via prenex-prefix classes and structure theories. It provides comprehensive decidability dichotomies for sentence classes across signatures—predicate-only and with function symbols, both with and without equality—and shows that optimization is undecidable when satisfiability is undecidable but decidable when solvability is decidable under suitable complexity measures. The work also offers constructive approaches to optimization under decidability assumptions and characterizes decidable classes through prefix forms, with implications for the design of computation-tree-based algorithms.
Abstract
In this paper, we study three algorithmic problems involving computation trees: the optimization, solvability, and satisfiability problems. The solvability problem is concerned with recognizing computation trees that solve problems. The satisfiability problem is concerned with recognizing sentences that are true in at least one structure from a given set of structures. We study how the decidability of the optimization problem depends on the decidability of the solvability and satisfiability problems. We also consider various examples with both decidable and undecidable solvability and satisfiability problems.