4
$\begingroup$

Context: Refering to the question: Complexity of the $(3,2)_s$ SAT problem? and since the paper by Porshen and Speckenmayer : Satisfiability of mixed Horn formulas, we know that even when $F_3$ is Horn, the problem of deciding the satisfiability of $F_3 \wedge F_2$ is NP-complete - where $F_3$ and $F_2$ are respectively 3-CNF and 2-CNF formulas.

I am wondering if there exist some cases where $F_3 \wedge F_2$ is easy to decide. Hence my question:

Let $F_3$ a 3-CNF containing only clauses with exactly 3 different literals and $F_2$ a 2-CNF defined on the same variables as $F_3$.

What is the complexity of deciding the satisfiability of $F_3 \wedge F_2$ when $F_3$ and $F_2$ are both monotone?

Thank you.

Improve this question
$\endgroup$
5
  • 1
    $\begingroup$ Anytime $F_2$ has few solutions, it is easy to find them, and this reduces the search space for $F_3$. More generally, I would expect some properties on the implication graph that $F_2$ represents to ensure that a tweaked DPLL runs fast. In this context, "few solutions" can probably be understood as "few strongly connected components". $\endgroup$
    – xavierm02
    Sep 5, 2020 at 6:51
  • $\begingroup$ I am confused about what assumptions you are making. Should I assume both 1 and 2; or are those two separate questions? If those are separate questions, it might be better to ask them separately. Should I assume $F_3$ is Horn in both of those cases, or was that just a motivating comment that should be ignored for the rest of the post? $\endgroup$
    – D.W.
    Sep 5, 2020 at 20:32
  • $\begingroup$ @D.W. That is two separate questions. The Horn introduction was just a motivating comment and should be ignored for the rest of the post. Sorry for the confusion. $\endgroup$
    – Xavier Labouze
    Sep 5, 2020 at 20:38
  • 1
    $\begingroup$ I encourage you to edit the question to make that clearer, and to post the second question separately. As you can see, you already got an answer that addresses the first of the two questions but not the second, so this will now be treated as an "answered" question and might be less likely to get attention for the second question. $\endgroup$
    – D.W.
    Sep 5, 2020 at 20:39
  • $\begingroup$ @D.W. Just did it. I removed the second part of the question since the first part is NP-complete - so is the second part. $\endgroup$
    – Xavier Labouze
    Sep 5, 2020 at 20:48

1 Answer 1

Reset to default
7
$\begingroup$

If $F_3$ and $F_2$ are both monotone, satisfiability can be checked in polynomial time (or even in coNLOGTIME), as $F_3\land F_2$, which is also monotone, is satisfiable iff it is satisfied by the $\vec1$ assignment, that is, iff it does not contain the empty clause.

If one of the formulas is allowed to be monotone and the other one negated monotone (i.e., having only negative literals), then satisfiability of $F_3\land F_2$ is NP-complete: given a 3-CNF $F$ in variables $x_1,\dots,x_n$, let $F_3$ be the monotone 3-CNF obtained from $F$ by replacing all negative literals $\neg x_i$ with new variables $y_i$, and let $F_2=\bigwedge_i(\neg x_i\lor\neg y_i)$. Then $F$ is equisatisfiable with $F_3\land F_2$.

In particular, if $(\vec x,\vec y)$ is a satisfying assignment for $F_3\land F_2$, then for each $i$, at most one of $x_i$ or $y_i$ gets value $1$, that is, $y_i\le\neg x_i$. Thus, if we modify the assignment so that $y_i:=\neg x_i$, it will still satisfy $F_3$ as it is monotone. It follows that $\vec x$ satisfies the original formula $F$.

Improve this answer
$\endgroup$
0

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.