Source-linked AI summary
Karp's NP-complete problems over first-order definable structures
Aidan Healy, Bartek Klin
TL;DR
The paper asks which of Karp’s NP-complete problems remain decidable on structures definable over equality atoms. It analyzes these problems through the structure of their legal solutions and finds a varied landscape: some are decidable, some undecidable, and some weighted problems are left untreated.
Problem
The paper determines the decidability of Karp’s NP-complete problems on structures that are infinite but first-order definable using equality alone.
Source: §1 · pp. 1–2Method
The paper views candidate solutions as relational expansions of the input and studies closure properties of legal solutions to establish decidability.
Source: §4 · p. 16Results
Seven of Karp’s 21 problems are undecidable, eleven are decidable, and three weighted problems are left without natural infinite versions.
Source: §1 · p. 3, §6 · p. 22Takeaways & Limitations
The problems exhibit varied behavior, and the paper presents techniques for analyzing computational problems in the definable setting.
Source: §8 · p. 29The complexity picture depends on the chosen input representation, and PSPACE-hard emptiness and equality testing obscure finer distinctions.
Source: §7.2 · p. 29
Abstract
from arXiv · showhide
We determine the decidability of Karp's NP-complete problems on structures which are first-order definable over the theory of equality, also known as orbit-finite sets with atoms or nominal sets.
1. Introduction
The paper asks how Karp’s classical decision problems behave on infinite structures definable using equality alone. Its results divide the problems into decidable, undecidable, and weighted cases without natural infinite extensions.
1. Introduction
- One ExactCover example admits a partitioning subfamily, but constructing it requires breaking the family’s symmetry, for instance by fixing an enumeration and proceeding inductively.At each step, the construction covers the first uncovered pair using a suitable third atom.Source: §1 · p. 1
- The target structures are generally infinite but finite up to bijective atom renaming, and their relations are first-order definable using equality alone.The paper calls these structures definable and uses sets with atoms to describe them.Source: §1 · p. 2
- The paper situates its setting between broader recursive structures, where all nontrivial questions become undecidable, and automatic structures, where some Karp problems are decidable and others remain undecidable.For automatic structures, Clique and SetPacking are decidable, while ExactCover and Hamiltonicity are undecidable.Source: §1 · p. 2
- Of Karp’s 21 problems, seven are undecidable, eleven are decidable, and three weighted problems lack natural infinite versions; decidable cases are PSPACE-complete or NEXP-complete under the chosen representation.The undecidable problems include CNFSat, ExactCover, and Hamiltonicity; decidable examples include VertexCover, while 3-Sat and Colorability were previously known decidable in this setting.Source: §1 · p. 3
2. Preliminaries: definable structures
The preliminaries introduce finite expressions for sets built from atoms and explain how these sets behave under atom renaming. They characterize definable sets through finite support and finitely many orbits.
2. Preliminaries: definable structures
- A set-builder expression forms sets from an expression and bound atom variables subject to a first-order condition using equality as its only relation symbol.Evaluating an expression under a valuation of its free variables gives a definable set; when the valuation’s image is S, the set is S-definable, and when S is empty it is equivariant.Source: §2 · p. 3
- Definable-set expressions support effective Boolean combinations, products, images, inverse images, quotients, and unions and intersections of definable families.The syntax can be extended with tuples, constants, set relations, and quantifiers over definable sets.Source: §2 · p. 4
- Atom automorphisms rename atoms consistently, and a finite set S supports a definable set when every automorphism fixing S leaves that set unchanged.Every definable set has a finite support, and its finite supports are closed under intersection, yielding a least support.Source: §2 · p. 4
- Definable sets are orbit-finite: each is a finite union of orbits under atom renaming that fixes its least support.The finite subsets of A are not orbit-finite because subsets of different sizes lie in different orbits.Source: §2 · pp. 4–5
- A brief excursion uses ordered atoms, taking A to be the rationals with order-preserving bijections as automorphisms.Definability, support, and orbit-finiteness are defined analogously, with the order relation added to the expression language.Source: §2 · p. 5
3. Undecidable problems
This section establishes undecidability for definable ExactCover, HittingSet, CNFSat, 0-1-ILP, directed and undirected Hamiltonicity, and 3D matching through reductions, including reductions from domino tiling. It also identifies restrictions under which ExactCover and HittingSet become decidable, and treats Hamiltonicity using doubly-infinite paths.
3.1. Exact cover.
- ExactCover is undecidable by an effective reduction from domino tiling, even when every set is finite; the construction has elements belonging to infinitely many tile sets.The reduction encodes grid tiles and their matching edges as exact-cover sets.Source: §3.1 · pp. 6, 9
- ExactTupleCover is undecidable, by converting finite-set ExactCover instances into equal-sized sets and then listing each set as a non-repeating tuple.The conversion preserves whether an exact cover exists.Source: §3.1 · p. 9
3.2. Hitting set, Satisfiability, 0-1 Integer Linear Programming.
- HittingSet is undecidable via an ExactCover reduction, and remains so when each element belongs to only finitely many sets in the family.The reduction swaps the roles of points and sets in the membership relation, so exact covers correspond to hitting sets.Source: §3.2 · p. 10
- CNFSat is undecidable by reduction from HittingSet, with satisfying assignments corresponding to hitting sets.The paper also gives an alternative direct reduction from satisfiability for the ∀∃ fragment of first-order logic.Source: §3.2 · p. 10
- Finite-clause CNFSat, HittingSet with finite sets in its family, and ExactCover where each element occurs in finitely many sets are decidable.These boundaries contrast with the undecidability results for unrestricted CNFSat, HittingSet, and ExactCover.Source: §3.2 · p. 11
- 0-1-ILP is undecidable by encoding each HittingSet constraint C as the equation summing its variables to 1.Solutions to the resulting equations are exactly hitting sets for the family.Source: §3.2 · p. 12
3.3. Hamiltonicity.
- DirectedHamiltonicity is undecidable: tuple gadgets can be traversed either visiting every tuple entry or visiting none, so the gadgets visited entry-first encode an exact cover.The reduction is from ExactTupleCover and constructs a graph with a doubly-infinite Hamiltonian path exactly when an exact cover exists.Source: §3.3 · pp. 12, 14
- UndirectedHamiltonicity is undecidable by converting each directed-graph vertex into an in–middle–out triple whose order enforces the directed traversal.For each directed edge (u, v), the construction adds an undirected edge from uout to vin.Source: §3.3 · p. 14
- The Hamiltonicity reductions also adapt to singly-infinite paths by adding initial vertices, including a modified construction for the directed-to-undirected reduction.A singly-infinite path has a starting point and extends to infinity in one direction.Source: §3.3 · p. 14
3.4. 3D matching.
- 3DMatching is undecidable by reduction from ExactTupleCover; the formulation also reduces the case A = B = C to arbitrary definable sets via their disjoint union.The earlier ExactCover reduction does not directly work in the definable setting.Source: §3.4 · p. 15
- In the 3D-matching reduction, the matching constraints force each tuple gadget to use either all entry-covering triples or the alternative triples, making the entry-covering tuples an exact cover.Conversely, an exact cover yields a matching by choosing entry-covering triples for its tuples and alternative triples for the others.Source: §3.4 · pp. 15–16
4. Decidability from extreme amenability
The section generalizes an extreme-amenability technique to decide several problems by showing that nonempty, downward-closed sets of legal solutions contain equivariant solutions. It establishes a compactness and fixed-point basis for this method, then applies it to satisfiability and graph problems.
4. Decidability from extreme amenability
- The method treats candidate solutions as relational expansions and uses downward closure to obtain an equivariant solution that can be searched for decidably.The section generalizes the technique used for finite-template constraint satisfaction problems.Source: §4 · p. 16
4.1. Compact sets of structures.
- Over ordered rational atoms with finitely many constants, every down-set of structures contains an equivariant structure.The proof uses compactness and extreme amenability; the associated spaces of structures and down-sets are compact.Source: §4.1 · p. 17
4.2. Decidability.
- 3-Sat is decidable by reducing the search to finitely many valuations that are constant on each orbit of variables.The satisfying valuations form a downwards-closed set, so when one exists an equivariant valuation exists.Source: §4.2 · p. 18
- CNFSat with finite clauses is decidable because each input has a computable upper bound on clause size, but unrestricted CNFSat can have satisfying valuations with no equivariant solution.The unrestricted case therefore need not satisfy the equivariant-solution step used by the method.Source: §4.2 · p. 18
- VertexCover, FeedbackVertexSet, and FeedbackArcSet are decidable using downward-closed sets of legal solutions.For a fixed finite solution, forbidden finite structures encode violations; for FeedbackVertexSet, an orbit-finite description of all forbidden structures is not required.Source: §4.2 · pp. 17, 19
- Colorability and, equivalently, CliqueCover are decidable by searching the computable finite set of equivariant colorings.Any finite coloring is a k-coloring for some k, and an equivariant coloring uses no more colors than the graph has vertex orbits.Source: §4.2 · p. 19
5. Other decidable cases
Several problems outside the downward-closed-solution method are nevertheless decidable on definable structures. The section decides Clique, SetPacking, and SetCovering, while noting that VertexCover has additional structure absent from general set coverings.
Clique
- Clique is decidable even though an infinite clique need not contain an equivariant clique.The proof uses equality-atom support and Ramsey’s theorem to reduce the question to whether an edge orbit supports infinitely many pairwise-adjacent vertices.Source: §5 · pp. 20–21
SetPacking
- SetPacking is decidable by reducing it to Clique on a graph whose vertices are sets and whose edges join disjoint sets.The decision question asks whether the family contains an infinite pairwise-disjoint subfamily.Source: §5 · p. 21
SetCovering
- SetCovering is decidable by searching for a set in the family that contains a suitably support-disjoint element; finitely many copies of that set then cover the domain.The proof reduces to a single infinite orbit and effectively searches for such an element and set.Source: §5 · p. 21
VertexCover
- The SetCovering argument also decides VertexCover, but the separate VertexCover proof reveals structure in its solution space that general set coverings lack.The reduction is the one used by Karp.Source: §5 · p. 21
6. Weighted problems
The paper adapts some weighted problems by replacing finite total weight with finiteness conditions, but notes that this can discard the role of weight values. It decides the resulting SteinerTree problem and gives a finiteness-based formulation of MaxCut, while leaving three other problems untreated.
SteinerTree
- SteinerTree is decidable by checking connectivity and whether the vertices in W lie in finitely many components after removing F.The proof computes transitive closure and then solves CliqueCover on the relevant components.Source: §6 · p. 22
Weighted problems
- A finite-total-weight reformulation can lose the essence of a weighted problem by ignoring weight magnitudes.For SteinerTree, the condition becomes equivalent to using only finitely many edges with nonzero weights.Source: §6 · p. 22
MaxCut
- The paper formulates MaxCut as asking whether some vertex subset has infinitely many F-edges crossing between it and its complement.The cited passage describes this as the infinite-setting version of the weighted problem.Source: §6 · p. 22
Untreated problems
- Knapsack, job sequencing, and number partitioning are left untreated because they seem less amenable to infinite generalizations.Source: §6 · p. 22
7. Complexity considerations
This section examines the complexity of the problems under different representations of definable structures, establishing PSPACE bounds for many problems and NEXP-completeness for 3-Sat and k-VertexCover with set-builder inputs. It describes reductions from succinct problems, including a polynomial-time construction of a definable graph isomorphic to a circuit-specified graph, and notes representation qualifications and fixed-dimension questions for future work.
7. Complexity considerations
- Set-builder expressions support many polynomial-time constructions but can be exponentially more compact than classical representations, while emptiness checking is PSPACE-complete.The paper therefore cautions that these complexity results depend on the representation scheme; an alternative orbit-based encoding can cause exponential blow-ups in products and representation length.Source: §7 · p. 23
7.1. Upper bounds.
- PSPACE algorithms handle basic definable-set operations and graph reachability, including emptiness, equality, membership, inclusion, orbit operations, support computation, and path existence.The path algorithm uses supports and orbit representatives to search a bounded path, with NPSPACE converted to PSPACE by Savitch’s theorem.Source: §7.1 · pp. 24–25
- 3-Sat has an NEXP upper bound by enumerating supported variable valuations, whereas several other problems achieve PSPACE bounds by avoiding storage of exponentially long solutions.For VertexCover, it suffices to check that every edge has an endpoint among the supported vertices; related orbit-based checks yield PSPACE bounds for FeedbackVertexSet, FeedbackArcSet, Colorability, and CliqueCover.Source: §7.1 · p. 25
- The cited results establish 3-Sat ∈ NEXP and show 3-Sat and k-VertexCover are NEXP-hard; VertexCover, FeedbackVertexSet, FeedbackArcSet, Colorability, CliqueCover, Clique, and SetPacking are in PSPACE.Source: §7.1 · pp. 25–26, §7.2 · p. 28
7.2. Lower bounds.
- The NEXP lower bounds for 3-Sat and k-VertexCover reduce their succinct classical versions to definable problems, with the reduction passing only through finite instances.For k-VertexCover, the construction produces in polynomial time a definable graph isomorphic to the graph encoded by the succinct input.Source: §7.2 · p. 28
- Binary sequences are encoded as atom-tuple orbits, yielding a definable graph isomorphic to the circuit-specified graph in polynomial time.Source: §7.2 · pp. 28–29
- Under the chosen input representation, the decidable Karp problems’ complexity is settled, but PSPACE-hard emptiness and equality mask finer distinctions; fixed-dimension NP questions remain open.The paper leaves for future work which Karp problems under various input representations become fixed-dimension NP.Source: §7.2 · p. 29
8. Conclusion
The conclusion frames Karp’s 21 problems as a principled survey whose behavior diverges sharply on definable structures. It maps that divergence onto Karp’s reduction tree and introduces a separate tree for undecidable problems.
8. Conclusion
- Choosing Karp’s famous, well-studied problems fixed the scope and forced examination of a range of properties shared by problems on finite structures.Their behavior on definable structures turned out to differ substantially.Source: §8 · p. 29
- The problems range from nontrivial undecidability to decidability for deep or mundane reasons, while Knapsack does not seem to generalize to definable structures.The conclusion presents the varied outcomes as a reason the fixed set of problems was a principled choice.Source: §8 · p. 29
- Figure 8 [Kar72, Fig. 1] marks decidable problems in green, undecidable ones in red, and weighted problems with missing or degenerate reformulations in gray.The problems that become undecidable are scattered across Karp’s tree, and few of its original reductions remain in force.Source: §8 · p. 29, Figure 8 · p. 30
- The authors introduce a distinct reduction tree for undecidable problems after finding that several of Karp’s original reductions break down in this setting.They were able to reuse a couple of the original reductions unchanged, including ExactCover to HittingSet.Source: §8 · p. 29, Figure 9 · p. 30
- The analysis of decidable problems and their complexity yields a small arsenal of techniques for studying simple computational problems in the definable setting.The new reduction tree for undecidable problems contributes to this broader landscape.Source: §8 · p. 29