# Common solutions to 3SAT and 2SAT models comprised of the same variables

I have a problem which is a combination of 3SAT & 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

• Sorry, it's not clear what you are asking. You say "the solution to the 2SAT instance". Is there a unique solution to the 2SAT instance? If so, the question is trivial: just use that solution. If not, the question is trivial: in the worst case it doesn't help. Also, the next sentence seems to contradict the previous sentence. Please edit the question to clarify exactly what you mean. – D.W. Sep 15 '20 at 5:44
• I have edited the question to provide better clarity. – gautam Sep 15 '20 at 12:12
• What are you looking for in an answer? As @D.W. points out, in the worst case the problem is as hard as 3-SAT, so NP-hard. Are you looking for heuristics? Are you wondering whether there is existing work on SAT solvers that might apply? Or maybe on average-case analysis of SAT? Also, what is "the DPLL solver"? – Neal Young Sep 15 '20 at 13:59

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.