Modified DPLL for 3-SAT by reducing to 2-SAT

Question

In Boolean Satisfiability of CNF formulae we have $k$-SAT where each clause has at most $k$ literals. It is well known that $k$-SAT is polynomial time reducible to $3$-SAT. It is also well known that $2$-SAT is solvable in polynomial time whereas $3$-SAT is NP-Complete (and therefore $k$-SAT $(k \gt 2)$ is NP-Complete by Cook's Theorem).

The Davis-Putnam-Logemann-Loveland (DPLL) algorithm is one of the earliest SAT solver algorithms. Here is the definition of the DPLL algorithm taken from Wikipedia.

Algorithm DPLL
    Input: A set of clauses φ
    Output: A truth value indicating whether φ is satisfiable.
Function DPLL(φ)
    While there is a unit clause {l} in φ do
        φ ← unit-propagate(l,φ);
    End While

    While there is a literal l that occurs pure in φ do
        φ ← pure-literal-assign(l,φ);
    End While

    If φ is empty then Return True; End If
    If φ contains an empty clause then Return False; End If

    l ← choose-literal(φ);

    Return DPLL(φ∧{l}) or DPLL(φ∧{¬l});
End Function

• ← denotes assignment.

• $\phi∧\{l\}$ denotes the simplification of $\phi$ after setting $l$ to True.

The options for solving strategy are in the last two lines of the algorithm, namely, the call to $\text{choose-literal}(\phi)$ and the short circuit evaluation in the Return statement $DPLL(\phi∧\{l\}) \text{ or } DPLL(\phi∧\{¬l\})$.

My question is about the approaches for reducing $3$-SAT to $2$-SAT using a modification of the DPLL.

Algorithm ModifiedDPLL
    Input: A set of clauses φ
    Output: A truth value indicating whether φ is satisfiable.
Function ModifiedDPLL(φ)
    While there is a unit clause {l} in φ do
        φ ← unit-propagate(l,φ);
    End While

    While there is a literal l that occurs pure in φ do
        φ ← pure-literal-assign(l,φ);
    End While

    If φ is empty then Return True; End If
    If φ contains an empty clause then Return False; End If
    If φ is a 2-SAT formula then Return 2SAT(φ); End If

    l ← choose-prolific-literal(φ);
    If l is empty (i.e., cannot be chosen) then Return False; End If

    (φ_min,φ_max) ← choose-minmax-sub-formula(φ∧{l},φ∧{¬l});
    
    Return ModifiedDPLL(φ_min) or ModifiedDPLL(φ_max);
End Function

The changes from the basic DPLL algorithm in the ModifiedDPLL algorithm are:

• We check if $\phi$ is a $2$-SAT formula (and this can be done in time linear in the number of clauses in $\phi$) and if so, we use the polynomial time $2$-SAT algorithm to determine the satisfiability of $\phi$.

• The branching rule $l ← \text{choose-literal}(\phi)$ in the original DPLL is modified to $l ← \text{choose-prolific-literal}(\phi)$ where we choose the literal that occurs in the maximum number of clauses in $\phi$. This greedy choice ensures that the recursive call in the next step can be intelligently evaluated.

• We compute the two subformulas by splitting $\phi \Leftrightarrow l \land \phi_{min} \lor \neg l \land \phi_{max}$ where $\phi_{min}$ has fewer $3$-SAT clauses than $\phi_{max}$. This selection is done in the line $(\phi_{min},\phi_{max}) ← \text{ choose-minmax-sub-formula}(\phi∧\{l\},\phi∧\{¬l\})$. Ties can be broken by choosing arbitrarily.

• Then we do a short-circuited recursive evaluation in $\text{Return ModifiedDPLL}(\phi_{min}) \text{ or ModifiedDPLL}(\phi_{max})$. This is greedy as we are choosing to recursively call the $\text{ModifiedDPLL}()$ function with the formula that has fewer $3$-SAT clauses first. We hope to get to a residual $2$-SAT formula that is either satisfiable or unsatisfiable.

If we have a residual $2$-SAT formula that is satisfiable, we can determine an assignment of truth values and combine it with the branch literal choices made so far and find the truth assignment for the original formula. Once a satisfiable assignment is found the algorithm terminates. If the residual $2$-SAT formula is unsatisfiable, then the second subformula is similarly evaluated for satisfiability until we find it either satisfiable or unsatisfiable.

Questions:

1. Is this a reasonable strategy?
2. Has this approach been used in the past. I reviewed the paper by M. Ouyang [MOuyang] and found that the branching rules reviewed in the paper used both clause length and the number of clauses. That paper is from 1998. Is there a more recent survey or SAT branching heuristics?

References:

[MOuyang]: Ming Ouyang. How good are branching rules in DPLL?, Discrete Applied Mathematics, Volume 89, Issues 1–3, 1998, Pages 281-286, ISSN 0166-218X, https://doi.org/10.1016/S0166-218X(98)00045-6.