Suppose we are given a standard first-order unification problem, represented as a set $D$ of term equality constraints, such that the system $D$ as a whole is unsatisfiable. Consider the minimal unsatisfiable constraint sets of this problem. (A set $C \subseteq D$ of type constraints is a minimal unsatisfiable constraint set if $C$ is unsatisfiable and every strict subset of $C$ is satisfiable.)

Define the involved set for $D$ as the set of all constraints in $D$ that are members of some minimal unsatisfiable constraint set—i.e. the union of all minimal unsatisfiable constraint sets. It would be very convenient if we could compute the involved set efficiently, because this is the set of constraints that are "involved" in making the problem instance unsatisfiable.

The question is, is it possible to compute the involved set for an arbitrary unification problem in polynomial time?

I've done some thought and research on this problem and haven't found a solution yet. In the remainder of this question, I will explain some of the ideas I have considered for solving the problem.

Independence systems

Since unification problems are constraint satisfaction problems, the satisfiable subsets of a given unification problem form an independence system. In the language of independence systems, a satisfiable constraint set is an independent set, an unsatisfiable constraint set is a dependent set, a maximal satisfiable constraint set is a base, and a minimal unsatisfiable constraint set is a circuit. Several algorithms in the literature on finding minimal unsatisfiable constraint sets in unification problems actually only need access to an oracle that supports efficiently testing at what point incrementally adding one constraint at a time to an independent set makes the set dependent. For example:

  • We can find a single arbitrary minimal unsatisfiable constraint set in $O(|D|^2)$ time. The algorithm to do this is described in Stuckey, Sulzmann, and Wazny (2003). "Interactive Type Debugging in Haskell", section 7.1.
  • Stuckey et al. (2003) also note that we can find the set of constraints that are members of every minimal unsatisfiable constraint set—i.e. the intersection of all minimal unsatisfiable constraint sets—in $O(|D|^2)$ time, because these are exactly the constraints $e \in D$ where $D \setminus \{ e \}$ is satisfiable.
  • We can use the existence of an incremental independence oracle to enumerate all of the minimal unsatisfiable constraint sets more efficiently than if we simply listed every subset of constraints and checked it for independence. For an example of such an algorithm, see Bailey and Stuckey (2005). "Discovery of Minimal Unsatisfiable Subsets of Constraints Using Hitting Set Dualization." Unfortunately, we can't simply enumerate all of the minimal unsatisfiable constraint sets and take their union explicitly, because a unification problem can have exponentially many minimal unsatisfiable sets.

I have not found an algorithm that allows computing the union of all circuits in polynomial time given only access to an incremental independence oracle, and my gut feeling is that it is probably not possible. (I'd love to be wrong on this.)

Because the satisfiable subsets of a unification problem form an independence system, it is natural to ask whether they also satisfy the exchange property so that they form a matroid. Unfortunately, in general they do not: $A = \{ a \sim \mathsf{Bool}, a \sim b, b \sim \mathsf{Bool} \}$ is an independent set that is larger than the independent set $B = \{ a \sim \mathsf{Int}, b \sim \mathsf{Float} \}$, but no element of $A \setminus B$ can be added to $B$ without making it dependent.

Type graphs and error paths

If the unification problem contains only constant and variable terms but no function symbols with arguments, then we can compute the involved set efficiently. This is because, in this restricted case, a constraint set is minimal unsatisfiable if and only if it is the set of edges comprising some simple path between two conflicting vertices in the type graph for the unification problem. (The concept of type graphs is described in detail in chapter 7 of Heeren (2005). Top Quality Type Error Messages.) Finding the set of all edges on any simple path between a subset of the vertices in a connected graph can be done in linear time by a straightforward reduction to the biconnected components problem for the graph.

Function symbols seem to make the problem more complicated, because the type graph can now contain exponentially-long shortest error paths (in the sense of Heeren (2005)). So if we want to find the involved set efficiently, we need a way of determining the set of edges that are on some error path between conflicting vertices without having to explicitly write down any error paths.

With function symbols, we also have to account for the possibility of occurs check errors in addition to function head clashes. Occurs check errors can be isolated efficiently by finding the strongly-connected components of the unified sets of the type graph, as described in Heeren (2005), but this doesn't give an involved set of constraints.

  • $\begingroup$ Why are you expecting this minimal set to be unique? Or are you just asking for a minimal set? $\endgroup$ – cody Jun 30 '17 at 12:45
  • 2
    $\begingroup$ @cody I am not expecting a unique minimal unsatisfiable set. I state explicitly that there can be exponentially-many such sets for a given input problem, and reference an algorithm for finding an arbitrary minimal unsatisfiable set. I am asking for an efficient way of calculating the union of all minimal unsatisfiable sets for a given input problem. $\endgroup$ – Aaron Rotenberg Jun 30 '17 at 17:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.