<p>Here is a paper by Porshen and Speckenmayer : <a href="https://www.sciencedirect.com/science/article/pii/S0166218X07000327" rel="nofollow noreferrer">Satisfiability of mixed Horn formulas</a> which shows that even when <span class="math-container">$F_3$</span> is Horn, the problem of deciding the satisfiability of <span class="math-container">$F_3 \wedge F_2$</span> is NP-complete.</p>

CC BY-SA 4.0
2023-12-13T16:11:32.437Z
Actually, as far as I understand, by Schaefer's dichotomy theorem, even when $F_3$ is XOR-3-SAT, it must be NP-complete. Same for when $F_3$ is monotone (and therefore trivially satisfiable). The reduction is known without having to refer to Schaefer's theorem, though.
rus9384
CC BY-SA 4.0
2023-12-14T17:24:23.890Z
Good point, you are right.
Xavier Labouze
CC BY-SA 4.0
2013-07-17T11:49:27.663Z
2022-05-12T10:30:01.803Z
2022-05-12T10:30:01.803Z
Xavier Labouze
<p>This problem is NP-complete.</p>

<p>Let $\varphi$ be an arbitrary CNF formula (an instance of SAT).  Consider $\varphi \lor y$, where $y$ is a fresh variable; obviously, this formula is satisfiable (you can simply set $y$ to true).  Now convert $\varphi \lor y$ to 3-CNF, using any standard method, and let $\psi$ denote the result.  Note that $\psi$ is a satisfiable 3-CNF formula, so we can let $F_3 = \psi$.  Now, let $F_2 = \neg y$.  Notice that $F_3 \land F_2$ is satisfiable if and only if $\varphi$ is.  Therefore, the $(3,2)_s$ SAT problem is at least as hard as SAT.  Also, it is clearly no harder than SAT.  Therefore, it is exactly as difficult as SAT.</p>

CC BY-SA 3.0
2013-07-15T18:15:45.623Z
Tks @D.W, quite convincing.
Xavier Labouze
CC BY-SA 3.0
2013-07-15T20:35:11.263Z
You should just reduce from 3SAT instead of from SAT.
Tyson Williams
CC BY-SA 3.0
2013-07-16T00:30:29.657Z
@TysonWilliams, yup, sure, we could do that too.  Is there any sense in which reducing from 3SAT would be better?   It doesn't seem to make any significant difference either way, as far as I can see.  Reducing from 3SAT doesn't seem to make the reduction any simpler.  Even if $\varphi$ is a 3-CNF formula, $\varphi \lor y$ won't be, so you still need to convert to 3-CNF either way.
D.W.
CC BY-SA 3.0
2013-07-18T18:46:33.973Z
Ah, yes.  Good point.
Tyson Williams
CC BY-SA 3.0
2013-07-15T17:30:06.717Z
2013-07-15T17:30:06.717Z
D.W.
<p>Let define the $(3,2)_s$ SAT problem : Given $F_3$, a satisfiable 3-CNF formula, and $F_2$, a 2-CNF formula ($F_3$ and $F_2$ are defined on the same variables). Is $F_3 \wedge F_2$ satisfiable?</p>

<p>What is the complexity of this problem ? (Has it been studied before ?)</p>

<cc.complexity-theory><reference-request><np-hardness><sat>
Complexity of the $(3,2)_s$ SAT problem?
Xavier Labouze
# Complexity of the $(3,2)_s$ SAT problem?

(Asked by: username_0 on 2013-07-15)

Let define the $(3,2)\_s$ SAT problem : Given $F\_3$, a satisfiable 3-CNF formula, and $F\_2$, a 2-CNF formula ($F\_3$ and $F\_2$ are defined on the same variables). Is $F\_3 \wedge F\_2$ satisfiable?

What is the complexity of this problem ? (Has it been studied before ?)

**Tags:** cc.complexity-theory, reference-request, np-hardness, sat


---

## 2 answers

### Answer by username_2 on 2013-07-15. Score: 14 | Accepted answer

This problem is NP-complete.

Let $\varphi$ be an arbitrary CNF formula (an instance of SAT). Consider $\varphi \lor y$, where $y$ is a fresh variable; obviously, this formula is satisfiable (you can simply set $y$ to true). Now convert $\varphi \lor y$ to 3-CNF, using any standard method, and let $\psi$ denote the result. Note that $\psi$ is a satisfiable 3-CNF formula, so we can let $F\_3 = \psi$. Now, let $F\_2 = \neg y$. Notice that $F\_3 \land F\_2$ is satisfiable if and only if $\varphi$ is. Therefore, the $(3,2)\_s$ SAT problem is at least as hard as SAT. Also, it is clearly no harder than SAT. Therefore, it is exactly as difficult as SAT.

> **Comments:**
> **username_0**: Tks @D.W, quite convincing.  
> **username_3**: You should just reduce from 3SAT instead of from SAT.  
> **username_2**: @TysonWilliams, yup, sure, we could do that too.  Is there any sense in which reducing from 3SAT would be better?   It doesn't seem to make any significant difference either way, as far as I can see.  Reducing from 3SAT doesn't seem to make the reduction any simpler.  Even if $\varphi$ is a 3-CNF formula, $\varphi \lor y$ won't be, so you still need to convert to 3-CNF either way.  
> **username_3**: Ah, yes.  Good point.  

---

### Answer by username_0 on 2013-07-17. Score: 2

Here is a paper by Porshen and Speckenmayer : [Satisfiability of mixed Horn formulas](https://www.sciencedirect.com/science/article/pii/S0166218X07000327) which shows that even when $F\_3$ is Horn, the problem of deciding the satisfiability of $F\_3 \wedge F\_2$ is NP-complete.

> **Comments:**
> **username_1**: Actually, as far as I understand, by Schaefer's dichotomy theorem, even when $F_3$ is XOR-3-SAT, it must be NP-complete. Same for when $F_3$ is monotone (and therefore trivially satisfiable). The reduction is known without having to refer to Schaefer's theorem, though.  
> **username_0**: Good point, you are right.  

---

