Monthly Archives: September 2020

Second Order Instantiation

This problem is from the same reference as last time’s but is a bit harder.

The problem: Second Order Instantiation.  This is problem LO19 from the appendix.

The description: Given two second order logic expressions E1 and E2.  E1 can have variables, E2 can’t.  Can we make a substitution of the variables in E1 to get an expression identical to E2?

Example: In second order predicate logic, functions can be variables.  So we could have E1 be P(X) ∧ P(Y), where P is a function variable, and X and Y are “regular” boolean variables.

If E2 was f(a) ∧ f(b) (where all of f, a, and b are not variables), then the substitution {P/f, X/a, Y/b} would work.  But if E2 was f(a) ∧ g(b), then no substitution would work.

Reduction: We again use the Baxter thesis that we used in the last problem to help us here.  We start with a SAT formula S (though really, there’s no reason why we couldn’t just use 3SAT) with n clauses C1 through Cn and m variables P1 through Pm.  E1 will contain one variable for each variable Pi in S, and one variable for each literal xi,j (clause i, position j in the clause).

We also create second-0rder variables gi, one for each clause in S.  Each function gi has degree equal to the number of literals in clause i.

E2 will be built out of the constant symbols T and F, and constant functions Gi, each Gi has degree equal to the number of literals in clause i.

We will also have an additional function H of degree 2, and K of degree 2n.

From each clause i, we build an expression ei‘ = H(gi(T,..T), gi(F,…F))

(Each gi has as many parameters as there are literals in clause i that are all either T or F)

We also build an expression Ei‘ = H(T,F)

For each clause i, literal j, define the expression ei,j”’ = gi(xi,j, …, pi,j, …, xi,j)

(All of the parameters are xi,j except for the jth one, which is the variable for pi,j)

We build the expression ei” = Gi(ei,j”’, …)

(Each Gi has as many parameters as there are literals in clause i)

We also build an expression Ei” = Gi(…)

Each parameter j is T if literal j if clause i is a positive occurrence of a variable, or it’s F if literal j of clause i is a negated occurrence of a variable.

We build E1 = K(e1‘, …, en‘, e1”, …, en”)

E2 = K(E1‘, …, En‘, E1”, …, En”)

Baxter was again good enough to give us an example.

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

E1 = K(H(g1(T), g1(F)),

H(g2(T,T), g2(F,F)),

H(g3(T), g3(F)),

H(g4(T,T,T), g4(F,F,F)),

G1(g1(p)),

G2(g2(p, x2,1), g2(x2,2, q)),

G3(g3(r)),

G4(g4(q, x4,1, x4,1), g4(x4,2, r, x4,2), g4(x4,3, x4,3, p)))

E2 = K(H(T,F), H(T,F), H(T,F), H(T,F),

G1(T), G2(F,T), G3(F), G4(F,T,F))

Let’s look at G1 to see how the substitution works.  We need G1(g1(p)) in E1 to map to G1(T) in E2.  So we need g1(p) to map to T.  From the first H function in E1, we also need g1(T) to map to T.  The only way to make both substitutions true is if the variable p is mapped to (or assigned to, in our SAT instance) to T.

Now let’s look at G4. We need the following three mappings to exist:

  • g4(q, x4,1, x4,1) -> F
  • g4(x4,2, r, x4,2) -> T
  • g4(x4,3, x4,3, p) ->F

..we already know from the H function that g4(T,T,T) maps to T and g4(F,F,F) maps to F.  We already know from our G1 discussion that p has to map to T.  For g4(x4,3, x4,3, p) to map to F, we’ll need x4,3 to map to F (and then we have g4(F,F,T) map to F.  Notice that because we move the “variable” parameter around g4, none of the other g4 clauses will be able to generate (F,F,T) parameters since they all have 2 copies of the same x variable in different places).

The actual proof of this reduction goes on for a couple of pages of the Baxter thesis, but hopefully this explains the basic idea.

Difficulty: 8.  This is harder to follow than last week’s, but the general idea of “binding variables and literals to functions that test for satisfiability” is a pattern we’ve seen several times.

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.