The next problem is one of the “Private Communication” problems. I’m going to try to take a stab at it myself.

**The problem: **Unification With Commutative Operators. This is problem AN16 in the appendix.

**The description: **Given a set V of variables, a set C of constants, a set of n ordered pairs (e_{i}, f_{i}) (1 ≤ i ≤ n) representing “expressions”. Each expression is defined recursively as either a variable from V, a constant from C, or (e+f) where e and f are expressions. Can we create a way to assign each variable v in V a variable-free expression I(v) such that, if I(e) denotes the expression obtained by making all such replacements of variables in an expression e, that I(e_{i}) ≡ I(f_{i}) for all i? We define e ≡ f as either:

- e = f (the only possible way if e or f is a constant)
- If e = (a+b) and f = (c + d) then either (a ≡ c and b ≡ d) or (a ≡ d and b ≡ c)

**Example: **Suppose C was {0,1}, and V was (x,y,z}. We will have pairs ((x+y), (0+1)) and ((y + z), (0 + 0)). Then substituting x with 1, and y and z with 0 makes the substituted pairs equivalent.

**Reduction: **I think this can be done with One-In-Three 3SAT. The SAT instance defines variables x_{1}..x_{k}. Each variable x_{i} in the SAT instance will correspond to 2 variables in the set V in our unification instance: x_{i} and ~x_{i}. Each clause in the SAT instance (l_{1}, l_{2}, l_{3}) will turn into the expression (e,f) where the “e side” is (l_{1}+l_{2}+l_{3}), where each l_{i} is the variable corresponding to the literal (i.e., either some x_{j} or some ~x_{j}). The “f side” of all expressions is (1+0+0), which corresponds to exactly one of the literals being true.

We also need to add some extra expressions to make sure that we set each x_{i} and ~x_{i} to opposite signs. So each variable x_{i} in the SAT instance gets a pair whose “e side” is (x_{i} + ~x_{i}), and whose “f side” is 0+1.

I think that the unification instance we’ve constructed has a solution if and only if we can find a way to:

- Set exactly one literal in each clause to true
- Set exactly one of x
_{i} and ~x_{i} to true, for all x_{i}

..which is exactly when the original One-In-Three 3SAT instance was solvable.

I’ll admit to being a little worried about whether this is correct, because the comment in G&J talked about there being at most 7 constants or variables in an expression, and I did it with just 3. Maybe it’s because I’m using One-In-Three 3SAT instead of regular 3SAT, or maybe I’m missing something.

**Difficulty: **4 if I’m right. I think starting from this version of 3SAT is a big hint.