Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.
Sign up to join this community
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 ?)
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.
Here is a paper by Porshen and Speckenmayer : Satisfiability of mixed Horn formulas which shows that even when $F_3$ is Horn, the problem of deciding the satisfiability of $F_3 \wedge F_2$ is NP-complete.
