4
$\begingroup$

I'm wondering whether the following SAT variant is NP-complete or polynomial. The formula given in input has n*m variables, and it has two parts.

A part with the n positive clauses: $$(x_{1,1} \lor \dots \lor x_{1,m}) \land \\\dots\\(x_{n,1} \lor \dots \lor x_{n,m})$$

And a part with negative clauses with two variables: $$ \neg x_{i,j} \lor \neg x_{k,l} $$ where $x_{i,j}$ and $x_{k,l}$ are part of the n*m variables mentioned above.

Thank you for the help

Improve this question
$\endgroup$
  • $\begingroup$ You say "almost" disjoint clauses. Does this mean that the number/structure of the two-variable clauses is somehow limited? $\endgroup$ – Niel de Beaudrap Oct 31 '14 at 23:01
  • 7
    $\begingroup$ This is NP-complete since it is equivalent to the multicolored clique problem. $\endgroup$ – daniello Oct 31 '14 at 23:55
  • $\begingroup$ No there is no restriction on the negative part (I said almost disjoint because the clauses is the positive part are disjoint) Thanks I'll look up the multicolored clique problem $\endgroup$ – Guest1444 Nov 1 '14 at 8:35
  • $\begingroup$ I guess in the graph for the multicolor clique, there is going to be an edge between two variables if they don't appear together in the negative part. Do you have a reference for the multicolor clique problem, when it is restricted to complements of interval graphs or to interval graphs (P or NP)? $\endgroup$ – Guest1444 Nov 2 '14 at 11:36
4
$\begingroup$

I don't know the Multicolored Clique Problem suggested by Daniello, however there is a simple reduction from 3SAT:

Given a 3SAT formula $\varphi$ over $n$ variables $x_1,...,x_n$; for each $x_i$ add two variables:

  • $y_{i}^T$ that represents $x_i = true$, and
  • $y_{i}^F$ that represents $x_i = false$

and add the clause $(\neg y_{i}^T \lor \neg y_{i}^F)$ that represents the condition that $x_i$ cannot be both true and false.

Finally replace every clause $C_j = (l_{j1} \lor l_{j2} \lor l_{j3})$ of $\varphi$ with a clause made of three positive literals $(y_{j1}^a \lor y_{j2}^b \lor y_{j3}^c)$ where:

  • $a = T$ if $l_{j1}= x_{j1}$, $b=F$ if $l_{j1} = \neg x_{j1}$
  • $b = T$ if $l_{j2}= x_{j2}$, $b=F$ if $l_{j2} = \neg x_{j2}$
  • $c = T$ if $l_{j3}= x_{j3}$, $b=F$ if $l_{j3} = \neg x_{j3}$

For example $(x_1 \lor \neg x_2 \lor \neg x_3)$ becomes: $(y_1^T \lor y_2^F \lor y_3^F)$

Update:

In order to make every positive literal $y_i$ (that can be $y_i^T$ or $y_i^F$) occur only once in the upper part, you can use the following technique:

Suppose that $y_i$ occurs twice, then you can simply replace the two occurrences with two new positive variables: $y_i'$ and $y_i''$ and add the conditions for: $y_i' \leftrightarrow y_i''$:

$$(\neg y_i' \lor y_i'') \land (\neg y_i'' \lor y_i')$$

At this point repeat the split procedure ($y_i'$ becomes $y_i^{T'}$ and $\neg y_i'$ becomes $y_i^{F'}$):

$$(\neg y_i^{T'} \lor \neg y_i^{F''}) \land (\neg y_i^{T''} \lor \neg y_i^{F'}) \land (y_i^{T'} \lor y_i^{F'}) \land (y_i^{T''} \lor y_i^{F''}) $$

and add a dum clause to the upper part in order to include the $y_i^{F'}$ and $y_i^{F''}$, for example: $(y_i^{F'} \lor y_i^{F''} \lor z_i)$, where $z_i$ is a new variable that can make the clause true.

If $y_i$ occurs more than twice the procedure is similar.

Improve this answer
$\endgroup$
  • $\begingroup$ Note that the variables in the positive part should all be distinct $\endgroup$ – Guest1444 Nov 2 '14 at 11:33
  • $\begingroup$ @Guest1444: ops, I didn't notice it. In that case it is enough to replace two (or more) positive occurrences of $y_i^T$ with two (or more) variables $y_i^{T'}, y_i^{T''}$ and add the clauses for $y_i^{T'} \leftrightarrow y_i^{T''}$: $(\neg y_i^{T'} \lor \neg y_i^{F''})$ and $(\neg y_i^{T''} \lor \neg y_i^{F'})$ ...(and add "dum" clauses to "include" $y_i^{F'}$ and $y_i^{F''}$ in the upper part; but the reduction is no more so straightforward :-S (I'll fix the answer tomorrow) $\endgroup$ – Marzio De Biasi Nov 2 '14 at 16:15

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.