A computational complexity analysis of tunable type inference for Generic Universe Types

We address questions related to the computational complexity of inferring types for a particular type system, Generic Universe Types (GUT) [1], [2], for Java programs. GUT is useful for many applications, such as program verification [3], thread synchronization, and memory management. However, requiring the programmer to explicitly provide type information is onerous, which motivates the problem of automatically inferring types. In contrast to classical type systems, ownership type systems such as GUT may have multiple typings that satisfy the type system's rules. It is therefore appropriate for the inference to be tunable — that is, the programmer can indicate preferences for certain typings via breakable constraints and/or by partial annotations. A question then is whether efficient algorithms exist for the type inference problem. In this work we establish the following results for the type inference problem for GUT [2]. (1) The tunable type inference problem that allows breakable constraints is NP-hard, (2) an encoding of the problem as boolean satisfiability (SAT), as in prior work, is indeed a polynomial-time reduction, (3) P ≠ NP implies that the problem is not approximable in polynomial time within an approximation ratio of n1−ϵ for any ϵ>0, and (4) while some restricted versions of the problem of practical interest, such as when breakable constraints are forbidden, are in P, others remain NP-hard. Our results justify the prior approach to the problem that is based on reduction to SAT. Apart from these results, given the observation in prior work that instances of the problem that arise in practice appear to be easy, we address the natural question as to what hard instances may look like, and whether they may arise in practice. We identify a class of hard instances of the problem by devising a method to generate such instances starting at instances of the Vertex Cover problem, which is known to be NP-hard. We then analyze the structural properties of such instances as compared to easy instances of similar size. We find that for the classes of instances we consider, certain SAT structural parameters may be predictive of empirical hardness.