10
$\begingroup$

A language $L$ is in the class $DP$ iff there are two languages $L1 \in NP$ and $L2 \in coNP$ such that $L = L1 \cap L2$

A canonical $DP$-complete problem is SAT-UNSAT : given two 3-CNF expressions, $F$ and $G$, is it true that $F$ is satisfiable and $G$ is not?

The Critical SAT problem is also known to be $DP$-complete : Given a 3-CNF expression $F$, is it true that $F$ is unsatisfiable but deleting any clause makes it satisfiable?

I am considering the following variant of the Critical SAT problem : Given a 3-CNF expression $F$, is it true that $F$ is satisfiable but adding any 3-clause (out of $F$ but using the same variables as $F$) makes it unsatisfiable? But I don't succeed in finding a reduction from SAT-UNSAT or even prove it is $NP$ or $coNP$ hard.

My question: is this variant DP-complete ?

Thank you for your answers.

$\endgroup$
  • $\begingroup$ I wasn't aware of DP: interesting class, especially if CRITICAL-SAT is complete for it. $\endgroup$ – Suresh Venkat Sep 13 '11 at 10:53
  • 1
    $\begingroup$ If there are two satisfying assigments $\tau\neq\tau' \vDash \varphi$, then $\varphi$ is not maximal. (assume that they differ on variable $p$, then $p$ is not implied by the formula and adding it or a clause containing it will not change satisfiability.) If we can find a clause not implied by the formula in polynomial time, we can add it's negation to the formula and simply using unit clause rule. Eventually we will find the value of all variables for a satisfying assignment. Then we just need to check if the formula is equivalent to the canonical formula for that assignment. $\endgroup$ – Kaveh Sep 13 '11 at 16:59
  • 1
    $\begingroup$ @Kaveh: I misunderstood your refined question. In your version of the question, “there is no clause that is not implied by the formula and can be added to it without making it unsatisfiable” is equivalent to the condition that there is exactly one satisfying assignment, and it is a standard US-complete (hence coNP-hard) problem. $\endgroup$ – Tsuyoshi Ito Sep 14 '11 at 14:19
  • 1
    $\begingroup$ Xavier: You are correct in that the language in @Kaveh’s version is a subset of the language in your version. But that does not imply reducibility between the two problems (in either direction). Remember that a reduction must map yes-instances to yes-instances and no-instances to no-instances. $\endgroup$ – Tsuyoshi Ito Sep 15 '11 at 12:28
  • 1
    $\begingroup$ Sorry, I wrote in the opposite direction. The language in your version is a subset of the language in Kaveh’s version. $\endgroup$ – Tsuyoshi Ito Sep 15 '11 at 12:47
2
$\begingroup$

[I made it into a proper answer b/c somebody gave it -1]

If any clause is allowed to be added, then the language is empty -- clearly to any satisfiable formula $F$ you can add a 3-clause $c$ made up of variables that do not appear in $F$: $F \cup \{ c \}$ will be satisfiable.

If the added clauses must use variables of $F$, then the language is in P.

Justification is as follows:

Take any $F \in L$, i.e. $F \in SAT$ and for any 3-clause $c$ on variables of $F$, $F \cup \{c\} \in UNSAT$. Say $c = l_1 \lor l_2 \lor l_3 \notin F$, where $l_i$ is a literal. Since $F \cup \{ c \}$ is UNSAT, all models of $F$ must have $l_i=0$ (for $i=1,2,3$) - because if some model had e.g. $l_1=1$, then it would satisfy $c$ and so $F \cup \{c\}$. Now, assume that there exists another clause $c'$ that is exactly like $c$, but with one or more literal flipped and such that $c' \notin F$, say $c' = \neg l_1 \lor l_2 \lor l_3$. Then by the same argument all models of $F$ must have $l_1 = 1$. Thus, the necessary condition for $F \in L$ is that for each clause $c \in F$ there are exactly 6 other clauses in $F$ that use the three variables of $c$ -- lets call these 7-clause subsets of $F$ blocks. Note that each block implies a unique satisfying assignment to its variables. When this necessary condition is satisfied, $F$ is either uniquely satisfiable or unsatisfiable. The two cases can be distinguished by testing whether the assignments implied by the blocks of $F$ clash, which can clearly be done in linear time.

$\endgroup$
  • 1
    $\begingroup$ Your observation is basically: to have the answer Yes, F must contain exactly seven out of the eight clauses on any choice of three distinct variables. Therefore finding the unique assignment (or detecting inconsistency) is easily done in polynomial time. $\endgroup$ – Tsuyoshi Ito Sep 14 '11 at 14:55
  • 2
    $\begingroup$ @Xavier: The two problems may look similar, but Anton’s observation shows that they are simply very different. This is very common in computational complexity. Typical examples include the comparison between 2SAT and 3SAT and between the Eulerian circuit and the Hamiltonian circuit. $\endgroup$ – Tsuyoshi Ito Sep 14 '11 at 15:40
  • 2
    $\begingroup$ @Xavier -- Tayfun's answer is incorrect. He shows that the problem is in DP -- its fine, any problem in P is automatically in DP. In order to show that the problem is DP-complete, he has to show reduction to another DP-complete problem (e.g. the first variant of Critical SAT). I submitted the edit to his answer, but its in the queue for "peer review". $\endgroup$ – Anton Belov Sep 15 '11 at 1:46
  • 3
    $\begingroup$ @Anton: Editing answers posted by other users drastically is usually not recommended. If you think Tayfun’s answer is fundamentally incorrect, you should not try to fix it by editing it. $\endgroup$ – Tsuyoshi Ito Sep 15 '11 at 11:57
  • 1
    $\begingroup$ It is very clear from SAT-UNSAT problem that for one formula you check for satisfiability for the other formula you check for unsatisfiability... In the original critical sat prpblem you do not take for granted that the given boolean formula is unsatisfiable. You have to check for it. Same with Xaviers version, you have to check that the given boolean formula is satisfiable. $\endgroup$ – Tayfun Pay Sep 15 '11 at 12:13
-1
$\begingroup$

May I propose an answer to my own question thanks to your comments : the variant of Critical SAT is in P.

Let us call "Problem 1" the variant of Critical SAT : Given a 3-CNF expression $F$, is it true that $F$ is satisfiable but adding any clause out of $F$ makes it unsatisfiable?

And "Problem 2" : Given a 3-CNF expression $F$ , is it true that $F$ contains all the clauses it implies and has a unique model ?

Given a 3-CNF formula, $F$ .

If $F$ is a yes instance of problem 2, then any clause out of $F$ is not implied by $F$ and then covers the only one possible satisfying assignment for $F$ . Adding such a clause to $F$ makes it unsastifiable. $F$ is consequently a yes instance of problem 1.

If $F$ is a no instance of problem 2, then : Case 1 : it exists a clause out of $F$ which is implied by $F$ . Then adding this clause to $F$ doesn't change its satisfiability. $F$ is consequently a no instance of problem 1. Case 2 : $F$ contains all the clauses it implies but is unsatisfiabe. $F$ is consequently a no instance of problem 1. Case 3 : $F$ contains all the clauses it implies but has at least 2 different models. As Kaveh's comment underlines it, « assume that the models differ on variable p, then adding a clause containing it will not change satisfiability. » $F$ is consequently a no instance of problem 1.

Then, $F$ is a yes instance of problem 1 iff $F$ is a yes instance of problem 2.

Problem 2 is clearly a P problem (for instance, $F$ is a yes instance of problem 2 iff there are exactly $\binom{n}{3}$ = $\frac{n(n-1)(n-2)}{3}$ clauses out of F with no opposite litterals in any two of them – $n$ is the number of variables). So is Problem 1.

$\endgroup$
  • 2
    $\begingroup$ You reworded the original problem to your liking. $\endgroup$ – Tayfun Pay Sep 23 '11 at 19:46
  • $\begingroup$ I am not sure about the 3-SAT version. Given a Boolean formula in CNF with M clauses and N variable, IF M=(3^N)-(2^N) then the given Boolean Formula is either UNSATISFIABLE or has only ONE Solution. Even so, to check for satisfiablity at that instance is still NP. There is no way your version is in P. $\endgroup$ – Tayfun Pay Sep 23 '11 at 19:58
  • 1
    $\begingroup$ @Xavier: This answer seems correct, but I think that it is the same as what Anton does in his answer. $\endgroup$ – Tsuyoshi Ito Sep 23 '11 at 20:20
  • $\begingroup$ @Tsuyoshi, you are right, just introducing Problem 2 whose first part (testing whether a formula contains all the clauses it implies) interests me - by the way, do you have any idea about the complexity of this first part ? $\endgroup$ – Xavier Labouze Sep 23 '11 at 21:34

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.