Splitting

Basic Splitting

In many applications there are clauses that can be split into components that do not share variables. It is then complete to refute all of the sets consisting of one component of the split and the remaining clauses. If any such split set is satisfiable, then the original set is also (obviously) satisfiable. Clauses derived in one refutation that are not dependant on the split component can be retained to be used in the next refutation, e.g., useful unit clauses might be kept. Splitting (i) shortens clauses, (ii) divides up the search space.

Example 
SS = { q(b),
       p(X) | r(X,Z),
       ~q(X) | ~s(X),
       ~p(X) | ~q(Y),
       s(Z) | ~r(X,Z) | ~q(W) }
The clause ~p(X) | ~q(Y) can be split, resulting in the two sets ... 
S1 = { q(b),
       p(X) | r(X,Z),
       ~q(X) | ~s(X),
       ~p(X),
       s(Z) | ~r(X,Z) | ~q(W) }
... and ... 
S2 = { q(b),
       p(X) | r(X,Z),
       ~q(X) | ~s(X),
       ~q(Y),
       s(Z) | ~r(X,Z) | ~q(W) }
S2 is trivially refutable. S1 can be treated recursively by splitting the clause s(Z) | r(X,Z) | ~q(W), resulting in ... 
S3 = { q(b),
       p(X) | r(X,Z),
       ~q(X) | ~s(X),
       ~p(X),
       s(Z) | ~r(X,Z) }
... and ... 
S4 = { q(b),
       p(X) | r(X,Z),
       ~q(X) | ~s(X),
       ~p(X),
       ~q(W) }
... each of which is refutable.

Splitting without Backtracking

Splitting as above was first done (in SPASS) by removing the clause being split, asserting one component of the split, refuting that, then back tracking to retract the split component and assert the next split component.

A later implementation (in Vampire) implements splitting without backtracking, by splitting clauses into two components, and adding a new propositional literal to one part and the negation of the literal to the other part. This approach shortens clauses, but is less effective at dividing up the search space. Useful clauses from one part of the search space are automatically used in other parts.

Example 
SS = { q(b),
       p(X) | r(X,Z),
       ~q(X) | ~s(X),
       ~p(X) | ~q(Y),
       s(Z) | ~r(X,Z) | ~q(W) }
The clause ~p(X) | ~q(Y) can be split, resulting in the set ... 
S1 = { q(b),
       p(X) | r(X,Z),
       ~q(X) | ~s(X),
       sp1 | ~p(X),
       ~sp1 | ~q(Y)
       s(Z) | ~r(X,Z) | ~q(W) }
S1 can be treated recursively by splitting the clause s(Z) | r(X,Z) | ~q(W), resulting in ... 
S3 = { q(b),
       p(X) | r(X,Z),
       ~q(X) | ~s(X),
       sp1 | ~p(X),
       ~sp1 | ~q(Y)
       sp2 | s(Z) | ~r(X,Z),
       ~sp2 | ~q(W) }
... which is refutable.

Ordered resolution needs to be used, with the ordering set up to make the new propositional literals last (smallest) in their clauses, e.g., for KBO make them light in ω and last in ρ.

Splitting with AVATAR

The AVATAR architecture uses a propositional ATP system to control the splitting. Each component of a split clause is tagged with a new propositional literal, and a propositional clause formed from the disjunction of the components' labels. The propositional clauses are passed to the propositional ATP system. If the propositional ATP system finds a model, the model is used to decide which components of the split clauses to use in the first-order part, i.e., controlling the order in which the components' sets are processed. If the propositional ATP system returns unsatisfiable, then it is known that the original set is unsatisfiable.

Example 
SS = { q(b),
       p(X) | r(X,Z),
       ~q(X) | ~s(X),
       ~p(X) | ~q(Y),
       s(Z) | ~r(X,Z) | ~q(W) }
The clauses ~p(X) | ~q(Y) and s(Z) | ~r(X,Z) | ~q(W) can be split. The components are tagged ... 
     ~p(X)                {sp1}
     ~q(Y)                {sp2}
     s(Z) | ~r(X,Z)       {sp3}
... and the propositional clauses that represent the split clauses are formed ... 
SP = { sp1 | sp2,
       sp3 | sp2 }
Note how the label sp2 is reused. The remaining clauses are tagged with a set of the propositions they depend upon (none initially). 
SF = { q(b),              {}
       p(X) | r(X,Z),     {}
       ~q(X) | ~s(X) }    {}
The propositional clauses are handed to the propositional ATP system, which returns a model, e.g., {~sp1,sp2,~sp3}. The model dictates that the clause components for positive elements of the model are be added to the clause set ... 
SF = { q(b),              {}
       p(X) | r(X,Z),     {}
       ~q(X) | ~s(X),     {}
       ~q(Y) }            {sp2}
Resolution of q(b) and ~q(Y) can then proceed, producing the empty clause that is dependent on {sp2}. This means that the propositional model cannot include sp2, which is enforced by adding ~sp2 to the set of propositional clauses ... 
SP = { sp1 | sp2,
       sp3 | sp2,
       ~sp2 }
The propositional ATP system produces a new model (necessarily) {sp1,~sp2,sp3}, and the clause set is correspondingly updated. Note that as sp2 is no longer true in the model, the corresponding changes are reversed ... 
SF = { q(b),              {}
       p(X) | r(X,Z),     {}
       ~q(X) | ~s(X),     {}
       ~p(X),             {sp1}
       s(Z) | ~r(X,Z) }   {sp3}
Resolution and subsumption produce ... 
SF = { q(b),              {}
       p(X) | r(X,Z),     {}
       ~q(X) | ~s(X),     {}
       ~p(X),             {sp1}
       s(Z) | ~r(X,Z) }   {sp3}
       ~s(b)              {}
       ~r(X,b)            {sp3}
       p(X)               {sp3}
       []                 {sp1,sp3}
Thus the model cannot contain sp1 and sp3, which is enforced by adding ~sp1 | ~sp3 to the set of propositional clauses ... 
SP = { sp1 | sp2,
       sp3 | sp2,
       ~sp2,
       ~sp1 | ~sp3 }
The propositional ATP system finds this set unsatisfiable, and the refutation is complete.

Clearly there are lots of control options to be implemented, and heuristics (e.g., which clauses to split, which propositional model to use, etc.) that will affect performance.

Exam Style Questions

  1. Use each of the three splitting techniques, and ordered resolution, refute this set ...

    Example, using KBO ω for clause and literal selection 
         S13 = { p(X) | ~q(X,Y) | ~s
             q(X,b) | r(X)
             ~r(a) | t(Z)
             s
             ~p(X) | ~s
             ~t(X) | ~s }