1
$\begingroup$

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

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – D.W. Sep 15 '20 at 5:44
  • $\begingroup$ I have edited the question to provide better clarity. $\endgroup$ – gautam Sep 15 '20 at 12:12
  • $\begingroup$ 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"? $\endgroup$ – Neal Young Sep 15 '20 at 13:59
1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ I am actually working on writing my own SAT solver and was wondering if I can use this form of the SAT problem as a "accelerator" to speed it up since I think I can transform any 3SAT problem into such a conjunction. I know that in the worst case the problem is still NP-hard so it is not useful for all cases, but I am wondering if it can still be useful in some cases. I am trying to code this up and if I can, I will profile and post my results. $\endgroup$ – gautam Sep 21 '20 at 15:48
  • 1
    $\begingroup$ The propagator of any modern SAT solver already fully utilizes binary implications. $\endgroup$ – Laakeri Oct 15 '20 at 17:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.