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

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

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

CC BY-SA 3.0
2017-08-01T01:57:36.693Z
To avoid duplication, can't you just make the second instance of $g$ on new variables?
Joshua Grochow
CC BY-SA 3.0
2017-08-01T05:27:50.040Z
@JoshuaGrochow Probably, but there is some case analysis involved.
Yuval Filmus
CC BY-SA 3.0
2017-08-01T18:10:51.487Z
What case analysis?
Radu GRIGore
CC BY-SA 3.0
2017-08-01T18:14:46.520Z
@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.
Yuval Filmus
CC BY-SA 3.0
2017-08-01T18:16:59.210Z
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.
Radu GRIGore
CC BY-SA 3.0
2017-08-01T18:19:36.947Z
@RaduGRIGore Right, that would be a simpler proof.
Yuval Filmus
CC BY-SA 3.0
2017-08-01T18:44:04.243Z
@RaduGRIGore: Indeed, that's what I had in mind :).
Joshua Grochow
CC BY-SA 3.0
2017-07-31T12:02:19.430Z
2017-08-01T18:19:11.347Z
2017-08-01T18:19:11.347Z
Yuval Filmus
<p>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?</p>

<cc.complexity-theory><complexity-classes><boolean-functions>
variant of Critical SAT
John
# variant of Critical SAT

(Asked by: username_0 on 2017-07-29)

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?

**Tags:** cc.complexity-theory, complexity-classes, boolean-functions


---

## 1 answers

### Answer by username_1 on 2017-07-31. Score: 8 | Accepted answer

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.

> **Comments:**
> **username_2**: To avoid duplication, can't you just make the second instance of $g$ on new variables?  
> **username_1**: @JoshuaGrochow Probably, but there is some case analysis involved.  
> **username_3**: What case analysis?  
> **username_1**: @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.  
> **username_3**: 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.  
> **username_1**: @RaduGRIGore Right, that would be a simpler proof.  
> **username_2**: @RaduGRIGore: Indeed, that's what I had in mind :).  

---

