# First Order Subsumption

The problem: First Order Subsumption.  This is problem LO18 in the appendix.

The description: (This definition is closer to the one in Baxter’s thesis than the on in G&J’s appendix because I think it’s easier to explain).

Given two sets of logic expressions A and B (A can contain variables, B can’t), does A subsume B?  A subsumes B if and only if we can create a substitution σ to the variables in A, then the result of applying that substitution to all expressions in A, which we call σ(A),  gives us a subset of B.

Example: Let A = {X,Y,f(Z)} B = {a,b,c,(f(d)}.  A subsumes B with the mapping {X->a, Y->b, Z->d}

Reduction: The PhD Thesis by Baxter has the reduction for this problem and the next one.  It is from 3SAT.

Given a 3SAT instance S, of which we have a set of variables U = {p1..pn}.  Our expressions will have those variables, the symbols T and F, and one function symbol Gi for each clause i.  The function will have as many parameters as the length of the clause (so, at most 3.  Baxter’s 3SAT definition allows for clauses with 1 or 2 literals).

Now, we build A.  Each clause i will create an expression Gi(pi1, pi2, pi3)- the parameters to the function are the variables corresponding to the literals of the clause.  A is the collection of all of those expressions.

Building B is harder. For each CNF clause Ci we list out all of the ways it can be satisfied by listing out the combinations of T and F we can give the variables in the clause.  So, for example, if our clause was (x1, x2, ~x3) we’d have

(T∧T∧T) ∨ (T∧T∧F) ∨ (T∧F∧T) ∨ (T∧F∧F) ∨ (F∧T∧T) ∨ (F∧T∧F) ∨ (F∧F∧F)

(We leave out  (F∧F∧T) because that represents the only way to set the variables that would not satisfy the clause).

We then wrap each of those possibilities with the Gi function for clause i.

Baxter was helpful enough to provide an example (This is pages 68-69 of the thesis):

Suppose S was: P ∧ (~P∨Q) ∧ ~R ∧ (~Q∨R∨~P).  We have 3 variables and 4 clauses.

A = {G1(P), G2(P,Q), G3(R), G4(Q,R,P)}.  The G symbols are functions and P, Q, and R are variables.

B = {G1(T),

G2(F,T), G2(F,F), G2(T,T),

G3(F),

G4(F,T,F), G4(F,T,T), G4(F,F,F), G4(F,F,T), G4(T,T,F), G4(T,T,T), G4(T,F,F)}

Notice that B has no variables, and a subsumption substitution will have to map variables to T or F.  Once we do that, we can see that a subsumption solution exists if and only if the original formula was satisfiable.

Difficulty: 6.  This is a pretty straightforward reduction.  The hard part is seeing how you want to replace variables with constants, how to use the function symbols, and how to take advantage of the “subset” rule in the subsumption definition to let you list out all possible ways to satisfy a clause.