8
$\begingroup$

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?

$\endgroup$
8
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ To avoid duplication, can't you just make the second instance of $g$ on new variables? $\endgroup$ – Joshua Grochow Aug 1 '17 at 1:57
  • 1
    $\begingroup$ What case analysis? $\endgroup$ – Radu GRIGore Aug 1 '17 at 18:10
  • 1
    $\begingroup$ @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. $\endgroup$ – Yuval Filmus Aug 1 '17 at 18:14
  • 3
    $\begingroup$ 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. $\endgroup$ – Radu GRIGore Aug 1 '17 at 18:16
  • 1
    $\begingroup$ @RaduGRIGore Right, that would be a simpler proof. $\endgroup$ – Yuval Filmus Aug 1 '17 at 18:19

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.