# variant of Critical SAT

The language Critical SAT is defined as the set of $CNF$ boolean formulas $f$ such that $f \in UNSAT$ but removing any clause from $f$ makes it satisfiable. It is known that Critical SAT is $DP$-complete. I wonder about the following variant: given a $CNF$ formula $f$, is it the case that $f$ is in $UNSAT$ and that there exists some clause $c$ such that $f \setminus c \in SAT$ (instead of for all clauses, there exists a clause). Is this variant $DP$-complete as well?

It is clear that your language is in DP. In order to show that it is DP-hard, we will give a reduction from SAT-UNSAT to your language, which we can call CRIT-UNSAT. Given a pair of CNFs $(f,g)$, let $x,y$ be fresh variables, and let $$h = (f \lor \lnot x) \land (g \lor x) \land (g \lor y) \land \lnot x \land (x \lor \lnot y).$$ Here $f \lor \lnot x$ means add $\lnot x$ to all clauses of $f$.
Suppose first that $f$ is satisfiable and $g$ is not satisfiable. Since $g$ is not satisfiable, $h$ is not satisfiable. Since $f$ is satisfiable, $h \setminus \lnot x$ is satisfiable. Thus $h$ is in CRIT-SAT.
Conversely, suppose that $h$ is in CRIT-SAT. Since $h$ is unsatisfiable, $g$ is unsatisfiable. For some clause $c$, $h \setminus c$ is satisfiable. If $c \in f \lor \lnot x$ then clearly $h \setminus c$ is still unsatisfiable. Similarly, if $c \in g \lor x$ then $h \setminus c$ is still unsatisfiable, due to $g \lor y$. If $c \in g \lor y$ or $c = x \lor \lnot y$ then $h \setminus c$ is still unsatisfiable, due to $g \lor x$. Thus $c = \lnot x$, which means that $h|_{x=1}$ is satisfiable, that is, $f$ is satisfiable.
• To avoid duplication, can't you just make the second instance of $g$ on new variables? Aug 1 '17 at 1:57
• @RaduGRIGore We can try $h = (f \lor \lnot x) \land (g \lor x) \land (g \lor y) \land \lnot x \land (x \lor \lnot y)$ for example. If $(f,g)$ is an instance of SAT-UNSAT then $h$ is unsatisfiable, and becomes satisfiable if we remove $\lnot x$. In the other direction, if $h$ is unsatisfiable then $g$ is unsatisfiable. We have to check that there is now way to "cheat" – to make it satisfiable by removing $x \lor \lnot y$, for example. Indeed, this won't help. But we had to check one more case. Aug 1 '17 at 18:14
• I thought what Joshua said is $h=(f\lor \lnot x)\land(g \lor x)\land(g'\lor x)\land\lnot x$, where $g'$ looks like $g$ but with primed variables. Aug 1 '17 at 18:16