<p>No, in general you cannot.  If <span class="math-container">$S_2(L) = (x_1 \lor \neg x_1)$</span>, say, then the implication graph for <span class="math-container">$S_2(L)$</span> gives you no information on the solutions to <span class="math-container">$S_3(L)$</span> or <span class="math-container">$B$</span>.</p>
<p>If you want to know how to solve it in practice, throw <span class="math-container">$B$</span> into a SAT solver.  No need to distinguish between the two types of clauses: SAT solvers already do everything there is to do.</p>

CC BY-SA 4.0
2020-09-21T15:48:11.923Z
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.
gautam
CC BY-SA 4.0
2020-10-15T17:43:49.697Z
The propagator of any modern SAT solver already fully utilizes binary implications.
Laakeri
CC BY-SA 4.0
2020-09-15T16:19:43.987Z
2020-09-15T16:19:43.987Z
D.W.
<p>I have a problem which is a combination of 3SAT &amp; 2SAT instances.
Consider <span class="math-container">$L$</span> is a set of variables <span class="math-container">$(x_1 ... x_n)$</span>. <span class="math-container">$S_3(L)$</span> is a 3-SAT instance and <span class="math-container">$S_2(L)$</span> is a 2SAT instance, both made of variables in L.
The actual boolean formula to solve is <span class="math-container">$B = S_3(L) \wedge S_2(L)$</span>. So the solution for B is an intersection of the solution sets of <span class="math-container">$S_3(L)$</span> and <span class="math-container">$S_2(L)$</span>.</p>
<p>Both <span class="math-container">$S_3$</span> and <span class="math-container">$S_2$</span> 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?</p>
<p>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?</p>
<p><em>Edited to better (hopefully) specify the problem</em></p>

CC BY-SA 4.0
2020-09-15T05:44:23.383Z
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.
CC BY-SA 4.0
2020-09-15T12:12:45.310Z
I have edited the question to provide better clarity.
gautam
CC BY-SA 4.0
2020-09-15T13:59:09.543Z
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
<cc.complexity-theory><sat><2sat>
Common solutions to 3SAT and 2SAT models comprised of the same variables
gautam
# Common solutions to 3SAT and 2SAT models comprised of the same variables

(Asked by: username_0 on 2020-09-14)

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*

**Tags:** cc.complexity-theory, sat, 2sat
> **Comments:**
> **username_1**: 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.  
> **username_0**: I have edited the question to provide better clarity.  
> **username_2**: 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"?  

---

## 1 answers

### Answer by username_1 on 2020-09-15. Score: 1

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.

> **Comments:**
> **username_0**: 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.  
> **username_3**: The propagator of any modern SAT solver already fully utilizes binary implications.  

---

