arXiv:2608.12206 · v3

Exponential Lower Bounds for Horn Amalgamation

首次提交 2026-08-13 00:01

版本更新 2026-11-09 22:48

雷达观测 2026-11-10 15:22

摘要

The amalgamation decision problem asks whether the finite models of a given universal first-order sentence have the amalgamation property. We prove that this problem is ExpTime-hard for universal Horn sentences of maximum relation arity three, and 2ExpTime-hard when the arity is unbounded, thereby strengthening the previous best lower bounds for universal Horn sentences. The first reduction simulates runs of nondeterministic tree automata using a single ternary relation and unary and binary auxiliary relations. The second simulates finite winning strategies in an exponential corridor game. As a secondary contribution, we prove that deciding the winner remains 2ExpTime-complete for the game normal form used in our reduction, in which each move label determines a unique legal successor from every non-winning legal row.

作者备注：The upper-bound claims in v2 have been withdrawn due to an error in the proof. This version focuses on the new lower bounds