Common solutions to 3SAT and 2SAT models comprised of the same variables I have a problem which is a combination of 3SAT &amp; 2SAT instances.
Consider $L$ is a set of variables $(x_1 ... x_n)$. $S_3(L)$ is a 3-SAT instance and $S_2(L)$ is a 2SAT instance, both made of variables in L.
The actual boolean formula to solve is $B = S_3(L) \wedge S_2(L)$. So the solution for B is an intersection of the solution sets of $S_3(L)$ and $S_2(L)$.
Both $S_3$ and $S_2$ can be solved separately, and then we can select a common solution to solve B. I was wondering if I can use the 2SAT solution to more efficiently solve the 3SAT instance, for e.g. can I use the implication graph from the solution of the 2SAT instance to guide the search for solution to the 3SAT instance?
I am aware we build an implication graph when solving a 3SAT instance through DPLL. So can we use an existing graph to guide the DPLL solver?
Edited to better (hopefully) specify the problem
No, in general you cannot.  If $S_2(L) = (x_1 \lor \neg x_1)$, say, then the implication graph for $S_2(L)$ gives you no information on the solutions to $S_3(L)$ or $B$.
If you want to know how to solve it in practice, throw $B$ into a SAT solver.  No need to distinguish between the two types of clauses: SAT solvers already do everything there is to do.