A variant of Critical SAT in DP

Question

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.

Answer 1

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

Answer 2

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.