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

<p>If <em>any</em> 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.</p>

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

<p>Justification is as follows:</p>

<p>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&#39;$ that is exactly like $c$, but with one or more literal flipped and such that $c&#39; \notin F$, say $c&#39; = \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$ <em>blocks</em>. 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.</p>

CC BY-SA 3.0
2011-09-13T17:01:06.983Z
I am not sure to agree with your answer. $F$ can have one model, say, $x=0$ for each variable in $F$, and be the conjuction of all clauses except clauses = (positive x,positive y,positive z) for all variables. Then adding any clause out of $F$ makes $F$ Unsatisfiable.
Xavier Labouze
CC BY-SA 3.0
2011-09-13T18:33:02.830Z
I think the only place where it breaks if when F is such that for any clause l1 v l2 v l3 (li are literals), the clause -l1 v l2 v l3 is in F, and so there are no second clause in my proof that is outside of F. The only example that comes to mind if you have 3 variables and 7 clauses. Not sure if there are more ...
Anton Belov
CC BY-SA 3.0
2011-09-13T19:01:55.663Z
You are allowing duplicates of a given clause... I do not think that is ok
Tayfun Pay
CC BY-SA 3.0
2011-09-13T19:04:26.623Z
@Xavier - come to think about it, your example is exactly the situation when there is no such pair of clauses ... so then, simply test F for SAT, if its SAT, then check if there are 2 different clauses on the same  variables that are not in F. If yes, then the formula is not in the language, if not, then yes.
Anton Belov
CC BY-SA 3.0
2011-09-13T21:07:42.397Z
@Anton : I am now in agreement with you. But, does stating that the langage is almost empty answer the question ?
Xavier Labouze
CC BY-SA 3.0
2011-09-13T21:50:37.517Z
@Xavier - hardly ;-) I will think about it
Anton Belov
CC BY-SA 3.0
2011-09-14T14:55:54.977Z
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.
Tsuyoshi Ito
CC BY-SA 3.0
2011-09-14T15:23:14.250Z
@Tsuyoshi - its the other direction: if it doesn't have 7 out of 8 clauses, then its not in the language (or, if its in the language, it has 7 out of 8 clauses). Its does not dismiss the possibility that there's a formula with 7 out of 8 clauses that is not in the language. Both directions are needed to show the language is in NP.
Anton Belov
CC BY-SA 3.0
2011-09-14T15:24:37.130Z
@Tsuyoshi : Right- my concern now is how to understand the gap of hardness between the original critical SAT problem and this variant which looks very similar ?
Xavier Labouze
CC BY-SA 3.0
2011-09-14T15:39:10.087Z
@Anton: Please try to understand why I wrote “(or detecting inconsistency)” in my previous comment.
Tsuyoshi Ito
CC BY-SA 3.0
2011-09-14T15:40:30.850Z
@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.
Tsuyoshi Ito
CC BY-SA 3.0
2011-09-14T20:16:47.507Z
@Tsuyoshi - ah, yes, of course: every such formula is either SAT with unique assignment if the "blocks" agree on intersecting variables, or UNSAT otherwise; sorry.
Anton Belov
CC BY-SA 3.0
2011-09-14T20:19:08.333Z
is this what they mean by "community answer" in FAQ ? ;-))
Anton Belov
CC BY-SA 3.0
2011-09-14T21:40:45.977Z
@Tsuyoshi - Tks for your comment. Yes, similarity doesn't mean equivalence. But it is easyer to me to understand the difference between 2SAT and 3SAT than between these two critical SAT problems.
Xavier Labouze
CC BY-SA 3.0
2011-09-15T00:13:39.713Z
@Xavier the first variant is about minimally unsatisfiable formulas - its a very strong property, because it means that *every* resolution refutation of F must use *all* clauses of F.
Anton Belov
CC BY-SA 3.0
2011-09-15T01:20:24.733Z
@Anton- I agree with you, but as Tayfun clarify it in his answer, the variant is also DP-complete - as NP is included in DP class, why not conclude P = NP so ?
Xavier Labouze
CC BY-SA 3.0
2011-09-15T01:46:16.920Z
@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".
Anton Belov
CC BY-SA 3.0
2011-09-15T03:19:39.900Z
@Anton My answer is not incorrect! I have revised my answer! Xaviers version  is indeed DP-Complete!
Tayfun Pay
CC BY-SA 3.0
2011-09-15T03:29:33.927Z
F(x)=(3^n)-(2^n)... If the number of clauses equals F(x) then the given Boolean formula in CNF is either uniquely satisfiable or unsatisfiable. Adding any clause that is not already in the given Boolean formula makes it unsatisfiable... Your instance is a weak version of that. Then I can ask you what happens when number of clauses are much less then that...
Tayfun Pay
CC BY-SA 3.0
2011-09-15T03:37:12.493Z
Please read papadimitriou's book. DP completeness is very clearly defined there. Either you have two formulas A and B and you ask if one is unsatisfiable and the other is satisfiable? Or you are given one formula, you ask if it is satisfiable or unsatisfiable at first. Then you either add or delete a clause and you ask the opposite question.  That is it.
Tayfun Pay
CC BY-SA 3.0
2011-09-15T09:53:22.757Z
@Tayfun : when the number of clauses are much less than F(x), then either the formula is not satisfiable or it exists at least one clause out of the formula which added to the formula doesn't change its positive satisfiability. In other words, in that case, the response to this variant of critical SAT is no.  Which shows its P membership...
Xavier Labouze
CC BY-SA 3.0
2011-09-15T11:47:42.653Z
P? How? You are in CNF form. You are adding an arbitary clause. Then checking for satisfiability... Your version is DP Complete no matter how you word it.
Tayfun Pay
CC BY-SA 3.0
2011-09-15T11:57:08.037Z
@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.
Tsuyoshi Ito
CC BY-SA 3.0
2011-09-15T12:04:50.737Z
@Anton, first you have to check to see if the givenboolean formula is satisfiable. So P=NP? I am done here...
Tayfun Pay
CC BY-SA 3.0
2011-09-15T12:13:55.077Z
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.
Tayfun Pay
CC BY-SA 3.0
2011-09-16T10:56:34.913Z
@Tayfun - let me try one last time, if this doesn't work I give up: take 2-SAT -- the language of satisfiable 2-CNF formulas. By your logic, 2-SAT is NP-complete, because "you have to check that the given formula is satisfiable". Yes, you are right, you have to check that it is satisfiable, *but* for the case of 2-CNF this check can be done in polytime. Hence $2-SAT \in P$. Note that since $P \subset NP$ (or, maybe, $P = NP$), $2-SAT$ is also in NP. But its *not* NP-complete.
Anton Belov
CC BY-SA 3.0
2011-09-16T12:24:40.877Z
@Anton. Please read page 415 of papadimitrious book. He is the one that defines class DP. There needs to be two different boolean formulas in cnf. First check if it is satisfiable then you check if the other one is unsatisfiable or other way around. Xaviers version just does the operations in reverse of the critical sat. It is clear from  unsat-sat it doesnt matter in which order you do it.. We do not know anything about the formulas before hand. We have to check if it is satisfiable or not.
Tayfun Pay
CC BY-SA 3.0
2011-09-16T12:31:01.247Z
Your version is pre determining what boolean formulas can be such that when we add a clause it becomes unsatisfiable. Then I could do that for any problem and say that i can solve it in linear.... No!!
Tayfun Pay
CC BY-SA 3.0
2011-09-16T16:28:10.750Z
@Tayfun, I read the book - your answer proves that this variant is in DP. If this variant is DP complete, what would be the reduction from SAT-UNSAT ? (because, in that case, such a reduction must exist).
Xavier Labouze
CC BY-SA 3.0
2011-09-16T20:10:00.060Z
For SAT-UNSAT there are two different Boolean formulas F & G. You check to see if F is satisfiable and if G is unsatisfiable! For Critical SAT,you have one formula. First you check to see if it is unsatisfiable, which corresponds to formula G in the SAT-UNSAT.  Then you delete one clause and check to see if it is satisfiable, which corresponds to formula F in SAT-UNSAT. In Xaviers version, first you check to see if it is satisfiable, which corresponds to formula F in SAT-UNSAT. Then you add one clause and check to see if it is unsatisfiable, which corresponds formula G SAT-UNSAT. OKAY?!?!?!
Tayfun Pay
CC BY-SA 3.0
2011-09-16T20:16:52.797Z
@Xavier. You see that there is no reduction, it is DP-Complete by definition!
Tayfun Pay
CC BY-SA 3.0
2011-09-20T10:30:03.057Z
@Tayfun, in "Christos H. Papadimitriou, David Wolfe, The complexity of facets resolved, Journal of Computer and System Sciences, Volume 37, Issue 1, August 1988, Pages 2-13", 
the authors proved the DP-completness of the original Critical SAT problem by finding a very subtle reduction from SAT-UNSAT. Why not to do the same here ?
Xavier Labouze
CC BY-SA 3.0
2011-09-20T13:02:59.247Z
@xavier, if you still do not see it I have nothing else to say. I am out of words. If you believe my answer is wrong then please check antons answer as correct.
Tayfun Pay
CC BY-SA 3.0
2011-09-23T21:38:08.107Z
@Anton, I proposed a similar answer to yours with a little difference in introducing an interesting "Problem 2".
Xavier Labouze
CC BY-SA 3.0
2011-09-13T16:20:46.593Z
2011-09-15T00:27:32.340Z
2011-09-15T00:27:32.340Z
Anton Belov
<p>May I propose an answer to my own question thanks to your comments : the variant of Critical SAT is in P. </p>

<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?</p>

<p>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 ?</p>

<p>Given a 3-CNF formula, $F$ .</p>

<p>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.</p>

<p>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.</p>

<p>Then, $F$ is a yes instance of problem 1 iff $F$ is a yes instance of problem 2. </p>

<p>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.</p>

CC BY-SA 3.0
2011-09-23T19:46:48.817Z
You reworded the original problem to your liking.
Tayfun Pay
CC BY-SA 3.0
2011-09-23T19:58:45.140Z
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.
Tayfun Pay
CC BY-SA 3.0
2011-09-23T20:20:19.070Z
@Xavier: This answer seems correct, but I think that it is the same as what Anton does in his answer.
Tsuyoshi Ito
CC BY-SA 3.0
2011-09-23T21:34:45.337Z
@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 ?
Xavier Labouze
CC BY-SA 3.0
2011-09-22T15:12:09.923Z
2011-09-22T23:30:59.323Z
2011-09-22T23:30:59.323Z
Xavier Labouze
<p>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$</p>

<p>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?</p>

<p>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?</p>

<p>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.</p>

<p>My question: is this variant DP-complete ?</p>

<p>Thank you for your answers. </p>

CC BY-SA 3.0
2011-09-13T10:53:46.650Z
I wasn't aware of DP: interesting class, especially if CRITICAL-SAT is complete for it.
Suresh Venkat
CC BY-SA 3.0
2011-09-13T13:10:26.447Z
@Kaveh -- its 3-CNF, so it has to be a 3-clause. It does not mean that the formula has one satisfying assignment -- a single 3-clause can block up to $2^{(|Var(F)|-3)}$ satisfying assignments.
Anton Belov
CC BY-SA 3.0
2011-09-13T14:37:48.860Z
@Kaveh : Any 3-clause out of the formula could be added. If the variant is in P, how to understand the gap of hardness between the classical "Critical SAT" and this variant ?
Xavier Labouze
CC BY-SA 3.0
2011-09-13T14:48:28.577Z
@Kaveh: I agree with you about this variant is in P.
Xavier Labouze
CC BY-SA 3.0
2011-09-13T14:53:11.397Z
@Kaveh -- ah ok, it seemed to me that OP is asking about "$F \in SAT$ and $\exists c, F \cup \{c \} \in UNSAT$". If the quantifier is universal, then, just like you said, the language is empty -- to any satisfiable 3-CNF formula $F$ add any clause with fresh variables (i.e. those that do not appear in $F$). The first version of Critical SAT problem is whether F is minimally unsatisfiable. Then, perhaps OP is asking about minimal correction subsets (MCS) ? Given an unsatisfiable $F$, a MCS of $F$ is $C \subset F$ such that $F \setminus C \in SAT$ and adding any clause *from $C$* to $F \setminus
Anton Belov
CC BY-SA 3.0
2011-09-13T15:49:39.863Z
@Anton: another possibility is: is the set of clauses a maximally consistent set of clauses? (i.e. there is no clause that is not implied by the formula and can be added to it without making it unsatisfiable). But even that might be easy to solve.
Kaveh
CC BY-SA 3.0
2011-09-13T15:55:14.910Z
I have just edited the question to clarify the issue about clause to add. Yes, the question is actually to know whether the set of clauses is a maximally consistent set of clauses. Tks Kaveh.
Xavier Labouze
CC BY-SA 3.0
2011-09-13T16:59:46.520Z
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.
Kaveh
CC BY-SA 3.0
2011-09-13T21:15:56.057Z
@Kaveh : Absolutly right, a "yes" answer to an instance of this variant of Critical SAT necessitates a formula with only one model (and then, it is easy to valid the definitive answer : yes or no)
Xavier Labouze
CC BY-SA 3.0
2011-09-14T13:25:16.367Z
@Kaveh: Why don’t you post it as an answer?
Tsuyoshi Ito
CC BY-SA 3.0
2011-09-14T14:19:07.863Z
@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](http://qwiki.stanford.edu/index.php/Complexity_Zoo:U#us)-complete (hence coNP-hard) problem.
Tsuyoshi Ito
CC BY-SA 3.0
2011-09-14T14:23:28.753Z
@Tsuyoshi, I didn't know about US and that this problem is complete for US. Thank you. (removing my previous reply.)
Kaveh
CC BY-SA 3.0
2011-09-14T14:27:04.567Z
Xavier, your question is different from what I wrote above (maximally consistent). If maximally consistent is what you are asking then check @Tsuyoshi's comment above.
Kaveh
CC BY-SA 3.0
2011-09-14T15:35:38.180Z
@Kaveh : Yet, I don't see the difference between your question and mine, do you ?
Xavier Labouze
CC BY-SA 3.0
2011-09-14T16:57:55.953Z
@Xavier, you are only excluding those clauses which are explicitly in the formula, mine excludes also clauses that are implied by the formula.
Kaveh
CC BY-SA 3.0
2011-09-15T01:37:33.707Z
Kaveh, Tsuyoshi, since the set of clauses not implied by the formula is included in the sets of clauses out of the formula (so in the set of clauses which can be added in the formula), do you mean that US is reducible to this variant of critical SAT (which would be co-NP hard and in P...) ?
Xavier Labouze
CC BY-SA 3.0
2011-09-15T01:45:53.133Z
@Xavier, no, I don't see how you can do that reduction, they are different problems. (ps: if a problem is coNP-hard and in P then P=NP. My version is unlikely to be in P, your version might be.)
Kaveh
CC BY-SA 3.0
2011-09-15T08:09:24.253Z
@Kaveh : Any instance of your version is an instance of mine, is n't ? (since the set of clauses not implied by the formula is included in the sets of clauses out of the formula (so in the set of clauses which can be added in the formula)
Xavier Labouze
CC BY-SA 3.0
2011-09-15T11:28:50.400Z
@Xavier, no, isn't. They are different questions.
Kaveh
CC BY-SA 3.0
2011-09-15T12:28:05.693Z
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.
Tsuyoshi Ito
CC BY-SA 3.0
2011-09-15T12:47:44.070Z
Sorry, I wrote in the opposite direction.  The language in your version is a subset of the language in Kaveh’s version.
Tsuyoshi Ito
<cc.complexity-theory><np-hardness><complexity-classes><sat>
A variant of Critical SAT in DP
Xavier Labouze
# A variant of Critical SAT in DP

(Asked by: username_0 on 2011-09-13)

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.

**Tags:** cc.complexity-theory, np-hardness, complexity-classes, sat
> **Comments:**
> **username_1**: I wasn't aware of DP: interesting class, especially if CRITICAL-SAT is complete for it.  
> **username_2**: @Kaveh -- its 3-CNF, so it has to be a 3-clause. It does not mean that the formula has one satisfying assignment -- a single 3-clause can block up to $2^{(|Var(F)|-3)}$ satisfying assignments.  
> **username_0**: @Kaveh : Any 3-clause out of the formula could be added. If the variant is in P, how to understand the gap of hardness between the classical "Critical SAT" and this variant ?  
> **username_0**: @Kaveh: I agree with you about this variant is in P.  
> **username_2**: @Kaveh -- ah ok, it seemed to me that OP is asking about "$F \in SAT$ and $\exists c, F \cup \{c \} \in UNSAT$". If the quantifier is universal, then, just like you said, the language is empty -- to any satisfiable 3-CNF formula $F$ add any clause with fresh variables (i.e. those that do not appear in $F$). The first version of Critical SAT problem is whether F is minimally unsatisfiable. Then, perhaps OP is asking about minimal correction subsets (MCS) ? Given an unsatisfiable $F$, a MCS of $F$ is $C \subset F$ such that $F \setminus C \in SAT$ and adding any clause *from $C$* to $F \setminus  
> **username_3**: @Anton: another possibility is: is the set of clauses a maximally consistent set of clauses? (i.e. there is no clause that is not implied by the formula and can be added to it without making it unsatisfiable). But even that might be easy to solve.  
> **username_0**: I have just edited the question to clarify the issue about clause to add. Yes, the question is actually to know whether the set of clauses is a maximally consistent set of clauses. Tks Kaveh.  
> **username_3**: 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.  
> **username_0**: @Kaveh : Absolutly right, a "yes" answer to an instance of this variant of Critical SAT necessitates a formula with only one model (and then, it is easy to valid the definitive answer : yes or no)  
> **username_4**: @Kaveh: Why don’t you post it as an answer?  
> **username_4**: @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](http://qwiki.stanford.edu/index.php/Complexity_Zoo:U#us)-complete (hence coNP-hard) problem.  
> **username_3**: @Tsuyoshi, I didn't know about US and that this problem is complete for US. Thank you. (removing my previous reply.)  
> **username_3**: Xavier, your question is different from what I wrote above (maximally consistent). If maximally consistent is what you are asking then check @Tsuyoshi's comment above.  
> **username_0**: @Kaveh : Yet, I don't see the difference between your question and mine, do you ?  
> **username_3**: @Xavier, you are only excluding those clauses which are explicitly in the formula, mine excludes also clauses that are implied by the formula.  
> **username_0**: Kaveh, Tsuyoshi, since the set of clauses not implied by the formula is included in the sets of clauses out of the formula (so in the set of clauses which can be added in the formula), do you mean that US is reducible to this variant of critical SAT (which would be co-NP hard and in P...) ?  
> **username_3**: @Xavier, no, I don't see how you can do that reduction, they are different problems. (ps: if a problem is coNP-hard and in P then P=NP. My version is unlikely to be in P, your version might be.)  
> **username_0**: @Kaveh : Any instance of your version is an instance of mine, is n't ? (since the set of clauses not implied by the formula is included in the sets of clauses out of the formula (so in the set of clauses which can be added in the formula)  
> **username_3**: @Xavier, no, isn't. They are different questions.  
> **username_4**: 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.  
> **username_4**: Sorry, I wrote in the opposite direction.  The language in your version is a subset of the language in Kaveh’s version.  

---

## 2 answers

### Answer by username_2 on 2011-09-13. Score: 3 | Accepted answer

[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.

> **Comments:**
> **username_0**: I am not sure to agree with your answer. $F$ can have one model, say, $x=0$ for each variable in $F$, and be the conjuction of all clauses except clauses = (positive x,positive y,positive z) for all variables. Then adding any clause out of $F$ makes $F$ Unsatisfiable.  
> **username_2**: I think the only place where it breaks if when F is such that for any clause l1 v l2 v l3 (li are literals), the clause -l1 v l2 v l3 is in F, and so there are no second clause in my proof that is outside of F. The only example that comes to mind if you have 3 variables and 7 clauses. Not sure if there are more ...  
> **username_5**: You are allowing duplicates of a given clause... I do not think that is ok  
> **username_2**: @Xavier - come to think about it, your example is exactly the situation when there is no such pair of clauses ... so then, simply test F for SAT, if its SAT, then check if there are 2 different clauses on the same  variables that are not in F. If yes, then the formula is not in the language, if not, then yes.  
> **username_0**: @Anton : I am now in agreement with you. But, does stating that the langage is almost empty answer the question ?  
> **username_2**: @Xavier - hardly ;-) I will think about it  
> **username_4**: 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.  
> **username_2**: @Tsuyoshi - its the other direction: if it doesn't have 7 out of 8 clauses, then its not in the language (or, if its in the language, it has 7 out of 8 clauses). Its does not dismiss the possibility that there's a formula with 7 out of 8 clauses that is not in the language. Both directions are needed to show the language is in NP.  
> **username_0**: @Tsuyoshi : Right- my concern now is how to understand the gap of hardness between the original critical SAT problem and this variant which looks very similar ?  
> **username_4**: @Anton: Please try to understand why I wrote “(or detecting inconsistency)” in my previous comment.  
> **username_4**: @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.  
> **username_2**: @Tsuyoshi - ah, yes, of course: every such formula is either SAT with unique assignment if the "blocks" agree on intersecting variables, or UNSAT otherwise; sorry.  
> **username_2**: is this what they mean by "community answer" in FAQ ? ;-))  
> **username_0**: @Tsuyoshi - Tks for your comment. Yes, similarity doesn't mean equivalence. But it is easyer to me to understand the difference between 2SAT and 3SAT than between these two critical SAT problems.  
> **username_2**: @Xavier the first variant is about minimally unsatisfiable formulas - its a very strong property, because it means that *every* resolution refutation of F must use *all* clauses of F.  
> **username_0**: @Anton- I agree with you, but as Tayfun clarify it in his answer, the variant is also DP-complete - as NP is included in DP class, why not conclude P = NP so ?  
> **username_2**: @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".  
> **username_5**: @Anton My answer is not incorrect! I have revised my answer! Xaviers version  is indeed DP-Complete!  
> **username_5**: F(x)=(3^n)-(2^n)... If the number of clauses equals F(x) then the given Boolean formula in CNF is either uniquely satisfiable or unsatisfiable. Adding any clause that is not already in the given Boolean formula makes it unsatisfiable... Your instance is a weak version of that. Then I can ask you what happens when number of clauses are much less then that...  
> **username_5**: Please read papadimitriou's book. DP completeness is very clearly defined there. Either you have two formulas A and B and you ask if one is unsatisfiable and the other is satisfiable? Or you are given one formula, you ask if it is satisfiable or unsatisfiable at first. Then you either add or delete a clause and you ask the opposite question.  That is it.  
> **username_0**: @Tayfun : when the number of clauses are much less than F(x), then either the formula is not satisfiable or it exists at least one clause out of the formula which added to the formula doesn't change its positive satisfiability. In other words, in that case, the response to this variant of critical SAT is no.  Which shows its P membership...  
> **username_5**: P? How? You are in CNF form. You are adding an arbitary clause. Then checking for satisfiability... Your version is DP Complete no matter how you word it.  
> **username_4**: @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.  
> **username_5**: @Anton, first you have to check to see if the givenboolean formula is satisfiable. So P=NP? I am done here...  
> **username_5**: 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.  
> **username_2**: @Tayfun - let me try one last time, if this doesn't work I give up: take 2-SAT -- the language of satisfiable 2-CNF formulas. By your logic, 2-SAT is NP-complete, because "you have to check that the given formula is satisfiable". Yes, you are right, you have to check that it is satisfiable, *but* for the case of 2-CNF this check can be done in polytime. Hence $2-SAT \in P$. Note that since $P \subset NP$ (or, maybe, $P = NP$), $2-SAT$ is also in NP. But its *not* NP-complete.  
> **username_5**: @Anton. Please read page 415 of papadimitrious book. He is the one that defines class DP. There needs to be two different boolean formulas in cnf. First check if it is satisfiable then you check if the other one is unsatisfiable or other way around. Xaviers version just does the operations in reverse of the critical sat. It is clear from  unsat-sat it doesnt matter in which order you do it.. We do not know anything about the formulas before hand. We have to check if it is satisfiable or not.  
> **username_5**: Your version is pre determining what boolean formulas can be such that when we add a clause it becomes unsatisfiable. Then I could do that for any problem and say that i can solve it in linear.... No!!  
> **username_0**: @Tayfun, I read the book - your answer proves that this variant is in DP. If this variant is DP complete, what would be the reduction from SAT-UNSAT ? (because, in that case, such a reduction must exist).  
> **username_5**: For SAT-UNSAT there are two different Boolean formulas F & G. You check to see if F is satisfiable and if G is unsatisfiable! For Critical SAT,you have one formula. First you check to see if it is unsatisfiable, which corresponds to formula G in the SAT-UNSAT.  Then you delete one clause and check to see if it is satisfiable, which corresponds to formula F in SAT-UNSAT. In Xaviers version, first you check to see if it is satisfiable, which corresponds to formula F in SAT-UNSAT. Then you add one clause and check to see if it is unsatisfiable, which corresponds formula G SAT-UNSAT. OKAY?!?!?!  
> **username_5**: @Xavier. You see that there is no reduction, it is DP-Complete by definition!  
> **username_0**: @Tayfun, in "Christos H. Papadimitriou, David Wolfe, The complexity of facets resolved, Journal of Computer and System Sciences, Volume 37, Issue 1, August 1988, Pages 2-13",  the authors proved the DP-completness of the original Critical SAT problem by finding a very subtle reduction from SAT-UNSAT. Why not to do the same here ?  
> **username_5**: @xavier, if you still do not see it I have nothing else to say. I am out of words. If you believe my answer is wrong then please check antons answer as correct.  
> **username_0**: @Anton, I proposed a similar answer to yours with a little difference in introducing an interesting "Problem 2".  

---

### Answer by username_0 on 2011-09-22. Score: -1

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.

> **Comments:**
> **username_5**: You reworded the original problem to your liking.  
> **username_5**: 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.  
> **username_4**: @Xavier: This answer seems correct, but I think that it is the same as what Anton does in his answer.  
> **username_0**: @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 ?  

---

